Solving open questions and other challenge problems using proof sketches

DOI10.1023/A:1010639725972MaRDI QIDQ5951528zbMATH OpenOpenAlexFDO

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:1010639725972

zbMATH Keywords

automated theorem provingcondensed detachmentlinked UR-resolutionproof sketchsearching for proofs in logical systems

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Finding shortest proofs: An application of linked inference rules
• Axiomatizing the skew Boolean propositional calculus
• Finding missing proofs with automated reasoning
• Missing proofs found
• scientific article; zbMATH DE number 2096993

Cited in

(13)

• Constructive logic with strong negation is a substructural logic. II
• A Wos Challenge Met
• A posthumous contribution by Larry Wos: excerpts from an unpublished column
• Compatibly involutive residuated lattices and the Nelson identity
• A Geometric Procedure with Prover9
• Loops with abelian inner mapping groups: an application of automated deduction
• Gibbard's collapse theorem for the indicative conditional: an axiomatic approach
• Proof simplification and automated theorem proving
• MOUFANG MAGMAS WITH INVERSES
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• Finding shortest proofs: An application of linked inference rules
• Axiomatizing the skew Boolean propositional calculus
• Constructive logic with strong negation is a substructural logic. I

Describes a project that uses

Uses Software

• Mizar

This page was built for publication: Solving open questions and other challenge problems using proof sketches

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