Finding missing proofs with automated reasoning

DOI10.1023/A:1012486904520MaRDI QIDQ5951893zbMATH OpenOpenAlexFDO

Authors Branden Fitelson, Larry Wos

Publication date 13 November 2002

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1012486904520

zbMATH Keywords

condensed detachmentautomated reasoning program OTTERlogic calculiaxiomatic proofs

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)

Recommendations

• Missing proofs found
• scientific article; zbMATH DE number 2100042
• Conquering the Meredith single axiom
• scientific article; zbMATH DE number 1865568
• scientific article; zbMATH DE number 2101984

Cited in

(7)

• Formalizing axiomatic systems for propositional logic in Isabelle/HOL
• Missing proofs found
• Solving open questions and other challenge problems using proof sketches
• scientific article; zbMATH DE number 2101984 (Why is no real title available?)
• Who finds the short proof?
• Double-negation elimination in some propositional logics
• Conquering the Meredith single axiom

Describes a project that uses

Uses Software

• OTTER

This page was built for publication: Finding missing proofs with automated reasoning

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