47 citations · 48 across the 3 of their papers we have counts for
3 papers
cs.LO2012★ 1 cited
Improved Separations of Regular Resolution from Clause Learning Proof Systems
Maria Luisa Bonet, Sam Buss, Jan Johannsen
We prove that the graph tautology formulas of Alekhnovich, Johannsen, Pitassi, and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned c…
cs.LO2008★ 47 cited
Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
Samuel R. Buss, Jan Hoffmann, Jan Johannsen
Resolution refinements called w-resolution trees with lemmas (WRTL) and with input lemmas (WRTI) are introduced. Dag-like resolution is equivalent to both WRTL and WRTI when there…
cs.LO2002
An Elementary Fragment of Second-Order Lambda Calculus
Klaus Aehlig, Jan Johannsen
A fragment of second-order lambda calculus (System F) is defined that characterizes the elementary recursive functions. Type quantification is restricted to be non-interleaved and…