A Resolution Calculus for Shortening Proofs

DOI10.1093/JIGPAL/JZI027MaRDI QIDQ5697719zbMATH OpenOpenAlexFDO

Authors Nicolas Peltier

Publication date 18 October 2005

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/jigpal/jzi027

zbMATH Keywords

extended resolution calculuslength of proofquantifier introduction method

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Recommendations

• scientific article; zbMATH DE number 1324437
• Short proofs are narrow -- resolution made simple
• Gentzen systems, resolution, and literal trees
• Short proofs are narrow—resolution made simple
• scientific article; zbMATH DE number 517073

Cited in

(7)

• Characterizing Tseitin-formulas with short regular resolution refutations
• Andrews Skolemization may shorten resolution proofs non-elementarily
• scientific article; zbMATH DE number 1324437 (Why is no real title available?)
• scientific article; zbMATH DE number 1342207 (Why is no real title available?)
• scientific article; zbMATH DE number 517073 (Why is no real title available?)
• Unsound inferences make proofs shorter
• scientific article; zbMATH DE number 5173934 (Why is no real title available?)

This page was built for publication: A Resolution Calculus for Shortening Proofs

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