Translation of resolution proofs into short first-order proofs without choice axioms
From MaRDI portal
Publication:2486578
DOI10.1016/J.IC.2004.10.011zbMATH Open1081.03014OpenAlexW2093910552MaRDI QIDQ2486578FDOQ2486578
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
Recommendations
Cut-elimination and normal-form theorems (03F05) Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- An optimality result for clause form translation
- Basic paramodulation
- Computing small clause normal forms
- Paramodulation-based theorem proving
- Lower bounds for increasing complexity of derivations after cut elimination
- Lower Bounds on Herbrand's Theorem
- Title not available (Why is that?)
- Normal form transformations
- Title not available (Why is that?)
- Automated proof construction in type theory using resolution
- Title not available (Why is that?)
- Translation of resolution proofs into short first-order proofs without choice axioms.
- Title not available (Why is that?)
Cited In (7)
- Scalable fine-grained proofs for formula processing
- Title not available (Why is that?)
- 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
- Title not available (Why is that?)
Uses Software
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)
