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)

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

• 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?)
• 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
• Meeting the challenge of fifty years of logic

Cited in

(6)

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

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)