Abstract
Resolution trees with lemmas (RTL) are a resolution-based propositional proof system that is related to the DPLL algorithm with clause learning. Its fragments are related to clause learning algorithms where the width of learned clauses is bounded by k. For every k up to O(log n), an exponential separation between the proof systems RTL(k) and RTL(k+1) is shown. © 2013 Springer-Verlag.
Cite
CITATION STYLE
Johannsen, J. (2013). Exponential separations in a hierarchy of clause learning proof systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7962 LNCS, pp. 40–51). https://doi.org/10.1007/978-3-642-39071-5_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
