Cut Elimination for the Second Order Propositional Logic with Hilbert's epsilon-symbol, Extensionality, and Full Comprehension. - Michael Gavrilovich (LFCS, 1997)

A Lower Bound for Interpolation. - Michael Gavrilovich (Log. J. IGPL, 1997)

MAX SAT approximation beyond the limits of polynomial-time approximation. - Evgeny Dantsin; Michael Gavrilovich; Edward A. Hirsch; Boris Konev (Ann. Pure Appl. Log., 2001)