scientific article; zbMATH DE number 4063061

MaRDI QIDQ3797157zbMATH OpenFDO

Authors Frank Pfenning

Publication date 1988

zbMATH Keywords

automated theorem proversaxiomatizations for propositional calculusfirst-order encodingfirst-order logicHypothetical SyllogismLukasiewicz shortest single axiomTarski-Bernays axioms

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• More proofs of an axiom of Łukasiewicz
• Shortest axiomatizations of implicational S4 and S5
• scientific article; zbMATH DE number 120344
• scientific article; zbMATH DE number 650883
• Conquering the Meredith single axiom

Cited in

(17)

• Investigations in protothetic
• Shortest axiomatizations of implicational S4 and S5
• Nice implicational axioms
• More proofs of an axiom of Łukasiewicz
• The shortest possible length of the longest implicational axiom
• Learning from Łukasiewicz and Meredith: investigations into proof structures
• The one variable implicational calculus
• Simplified Axiom Schemes for Implication and Iterated Implication
• scientific article; zbMATH DE number 5147179 (Why is no real title available?)
• scientific article; zbMATH DE number 120344 (Why is no real title available?)
• scientific article; zbMATH DE number 1471997 (Why is no real title available?)
• scientific article; zbMATH DE number 804148 (Why is no real title available?)
• Conquering the Meredith single axiom
• Partheo: A high-performance parallel theorem prover
• Automated reasoning contributes to mathematics and logic
• Investigations into proof structures
• Axiomatizing the skew Boolean propositional calculus

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 Q3797157)