The relative complexity of resolution and cut-free Gentzen systems

DOI10.1007/BF01531026zbMath0865.03011OpenAlexW2013167486MaRDI QIDQ1353988

Alasdair Urquhart

Publication date: 13 May 1997

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01531026

zbMATH Keywords

simulationresolutionrelative efficiencyclassical propositional calculuscut-free Gentzen systemproof systems for biconditionals

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15) Classical propositional logic (03B05) Proof theory in general (including proof-theoretic semantics) (03F03) Complexity of proofs (03F20)

Related Items

Simulation of Natural Deduction and Gentzen Sequent Calculus ⋮ Relative efficiency of propositional proof systems: Resolution vs. cut-free LK ⋮ A Logical Autobiography

Cites Work

• Seventy-five problems for testing automatic theorem provers
• On the complexity of regular resolution and the Davis-Putnam procedure
• The complexity of Gentzen systems for propositional logic
• Toward Mechanical Mathematics
• Hard examples for resolution
• The relative efficiency of propositional proof systems
• Unnamed Item

This page was built for publication: The relative complexity of resolution and cut-free Gentzen systems