Searching for circles of pure proofs

DOI10.1007/BF00881802MaRDI QIDQ1904397zbMATH OpenWikidataFDO

Authors Larry Wos

Publication date 20 December 1995

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

Full work available at URL https://doi.org/10.1007/BF00881802

zbMATH Keywords

automated reasoningpure proofs

Mathematics Subject Classification ID

Recommendations

• OTTER and the Moufang identity problem
• Missing proofs found
• Shortest single axioms for the equivalential calculus with CD and RCD
• Conquering the Meredith single axiom
• scientific article; zbMATH DE number 2100042

Cites work

• A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains
• A shortest single axiom for the classical equivalential calculus
• Complexity and related enhancements for automated theorem-proving programs
• Condensed detachment as a rule of inference
• scientific article; zbMATH DE number 41806 (Why is no real title available?)
• scientific article; zbMATH DE number 1348483 (Why is no real title available?)
• scientific article; zbMATH DE number 590572 (Why is no real title available?)
• Meeting the challenge of fifty years of logic

Cited in

(8)

• Shortest single axioms for the equivalential calculus with CD and RCD
• Shortest axiomatizations of implicational S4 and S5
• Proofs as schemas and their heuristic use
• OTTER and the Moufang identity problem
• Larry Wos: visions of automated reasoning
• Experiments in the heuristic use of past proof experience
• CODE: A powerful prover for problems of condensed detachment
• A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains

Describes a project that uses

Uses Software

• OTTER

This page was built for publication: Searching for circles of pure proofs

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