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

automated reasoning program OTTERaxiomatic proofscondensed detachmentlogic calculi

Mathematics Subject Classification ID

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

Review text

The paper focuses on finding axiomatic proofs by using the automated reasoning program OTTER. Many of the proofs the authors have found are missing in the literature on logic. An example of such a missing proof concerns the Łukasiewicz 23-letter single axiom for two-valued calculus. Many of the proofs answer questions that remained open for decades.

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
• scientific article; zbMATH DE number 2101984 (Why is no real title available?)
• Solving open questions and other challenge problems using proof sketches
• Conquering the Meredith single axiom
• Missing proofs found
• Who finds the short proof?
• Double-negation elimination in some propositional logics

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)