scientific article; zbMATH DE number 5147179

MaRDI QIDQ3433180zbMATH OpenFDO

Authors Larry Wos, Dolph Ulrich, Branden Fitelson

Publication date 27 April 2007

zbMATH Keywords

automated reasoningcondensed detachmentCXMdetachmentequivalenceequivalential calculusOTTERshortest single axiomssingle axiomsXCB

Mathematics Subject Classification ID

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

Recommendations

• Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus
• Shortest single axioms for the equivalential calculus with CD and RCD
• \textbf{D}-complete axioms for the classical equivalential calculus
• scientific article; zbMATH DE number 3045411
• A finitely axiomatized formalization of predicate calculus with equality
• scientific article; zbMATH DE number 167189
• Completeness of the ZX-calculus
• scientific article; zbMATH DE number 1159511
• scientific article; zbMATH DE number 4063061
• Computer Science Logic

Cited in

(5)

• Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus
• Larry Wos: visions of automated reasoning
• \textbf{D}-complete axioms for the classical equivalential calculus
• Remarks on Dudek's E-groupoids
• D-complete single axioms for the equivalential calculus with the rules d and r

Describes a project that uses

Uses Software

• OTTER

This page was built for publication:

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