Buss, Samuel R.; Hoffmann, Jan; Johannsen, Jan Resolution trees with lemmas: resolution refinements that characterize DLL algorithms with clause learning. (English) Zbl 1159.03009 Log. Methods Comput. Sci. 4, No. 4, Paper 13, 28 p. (2008). MSC: 03B35 03F20 68T15 68T20 PDFBibTeX XMLCite \textit{S. R. Buss} et al., Log. Methods Comput. Sci. 4, No. 4, Paper 13, 28 p. (2008; Zbl 1159.03009) Full Text: DOI
Beckmann, Arnold; Johannsen, Jan An unexpected separation result in linearly bounded arithmetic. (English) Zbl 1065.03039 Math. Log. Q. 51, No. 2, 191-200 (2005). MSC: 03F30 03F20 68Q15 PDFBibTeX XMLCite \textit{A. Beckmann} and \textit{J. Johannsen}, Math. Log. Q. 51, No. 2, 191--200 (2005; Zbl 1065.03039) Full Text: DOI
Johannsen, Jan Equational calculi and constant depth propositional proofs. (English) Zbl 0890.03031 Beame, Paul W. (ed.) et al., Proof complexity and feasible arithmetics. Papers from the DIMACS workshop, Rutgers, NJ, USA, April 21–24, 1996. Providence, RI: American Mathematical Society. DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 39, 149-162 (1998). MSC: 03F20 68Q15 03F30 03D20 03B05 PDFBibTeX XMLCite \textit{J. Johannsen}, DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 39, 149--162 (1998; Zbl 0890.03031)