Translation of resolution proofs into short first-order proofs without choice axioms

DOI10.1016/j.ic.2004.10.011zbMath1081.03014OpenAlexW2093910552MaRDI QIDQ2486578

Hans de Nivelle

Publication date: 5 August 2005

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2004.10.011

zbMATH Keywords

Theorem provingProof theorySkolemization

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Complexity of proofs (03F20)

Related Items (3)

On the mechanization of the proof of Hessenberg's theorem in coherent logic ⋮ Rocket-Fast Proof Checking for SMT Solvers ⋮ Scalable fine-grained proofs for formula processing

Uses Software

• ACL2
• Ivy

Cites Work

• Lower bounds for increasing complexity of derivations after cut elimination
• An optimality result for clause form translation
• Automated proof construction in type theory using resolution
• Basic paramodulation
• Lower Bounds on Herbrand's Theorem
• Automated Deduction – CADE-19
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Translation of resolution proofs into short first-order proofs without choice axioms