Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus

DOI10.1023/A:1021693818601MaRDI QIDQ1869616zbMATH OpenOpenAlexFDO

Authors Larry Wos, Dolph Ulrich, Branden Fitelson

Publication date 28 April 2003

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

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

zbMATH Keywords

automated reasoningcondensed detachmentdetachmentequivalenceequivalential calculusOTTERshortest single axiomssingle axiomsXCB

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35)

Review text

This paper answers the following question: Is the formula \(\text{XCB}= e(x,e(e(e(xy)\), \(e(z,y)),z))\) a single axiom for the classical equivalential calculus when the rules of inference consist of detachment and substitution? Heretofore, thirteen shortest single axioms for classical equivalence of length eleven have been discovered, and XCB was the only remaining formula whose status was undetermined. This result ends the search for shortest single axioms for the equivalential calculus.

Recommendations

• scientific article; zbMATH DE number 5147179
• Shortest single axioms for the equivalential calculus with CD and RCD
• scientific article; zbMATH DE number 650883
• A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains
• Short single axioms for Boolean algebra

Cited in

(5)

• Shortest single axioms for the equivalential calculus with CD and RCD
• Larry Wos: visions of automated reasoning
• scientific article; zbMATH DE number 5147179 (Why is no real title available?)
• A method for finding new sets of axioms for classes of semigroups.
• Computer theorem proving in mathematics

Describes a project that uses

Uses Software

• OTTER

This page was built for publication: Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus

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