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

DOI10.1016/J.IC.2004.10.011MaRDI QIDQ2486578zbMATH OpenOpenAlexFDO

Authors 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

Proof theorySkolemizationTheorem proving

Mathematics Subject Classification ID

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

Recommendations

• Translation of resolution proofs into short first-order proofs without choice axioms.
• A Compressing Translation from Propositional Resolution to Natural Deduction
• scientific article; zbMATH DE number 4037813
• A structure-preserving clause form translation
• Resolution is cut-free

Cites work

• scientific article; zbMATH DE number 1614692 (Why is no real title available?)
• scientific article; zbMATH DE number 424614 (Why is no real title available?)
• scientific article; zbMATH DE number 3871342 (Why is no real title available?)
• scientific article; zbMATH DE number 627412 (Why is no real title available?)
• scientific article; zbMATH DE number 1948188 (Why is no real title available?)
• scientific article; zbMATH DE number 2090295 (Why is no real title available?)
• An optimality result for clause form translation
• Automated proof construction in type theory using resolution
• Basic paramodulation
• Computing small clause normal forms
• Lower Bounds on Herbrand's Theorem
• Lower bounds for increasing complexity of derivations after cut elimination
• Normal form transformations
• Paramodulation-based theorem proving
• Translation of resolution proofs into short first-order proofs without choice axioms.

Cited in

(7)

• Scalable fine-grained proofs for formula processing
• scientific article; zbMATH DE number 4037813 (Why is no real title available?)
• Translation of resolution proofs into short first-order proofs without choice axioms.
• Rocket-Fast Proof Checking for SMT Solvers
• Andrews Skolemization may shorten resolution proofs non-elementarily
• On the mechanization of the proof of Hessenberg's theorem in coherent logic
• scientific article; zbMATH DE number 4043813 (Why is no real title available?)

Describes a project that uses

Uses Software

• Ivy
• ACL2

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2486578)