Finding shortest proofs: An application of linked inference rules

DOI10.1023/A:1010635625063MaRDI QIDQ5951526zbMATH OpenFDO

Authors Robert Veroff

Publication date 7 January 2002

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/A:1010635625063

zbMATH Keywords

automated theorem provingcondensed detachmentlinked UR-resolutionsearching for shortest proofs in logical systems

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Solving open questions and other challenge problems using proof sketches
• The search efficiency of theorem proving strategies
• Condensed detachment as a rule of inference
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• The linked inference principle. I: The formal treatment

Cited in

(7)

• Learning from Łukasiewicz and Meredith: investigations into proof structures
• Theorem proving as constraint solving with coherent logic
• Proof simplification and automated theorem proving
• Solving open questions and other challenge problems using proof sketches
• Lemmas: generation, selection, application
• Short proofs of ideal membership
• Investigations into proof structures

This page was built for publication: Finding shortest proofs: An application of linked inference rules

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