Searching for circles of pure proofs

DOI10.1007/BF00881802zbMATH Open0838.68101WikidataQ114267040 ScholiaQ114267040MaRDI QIDQ1904397FDOQ1904397

Authors: Larry Wos 

Publication date: 20 December 1995

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

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

zbMATH Keywords

automated reasoningpure proofs

Mathematics Subject Classification ID

Cites Work

• Title not available (Why is that?)
• A shortest single axiom for the classical equivalential calculus
• Complexity and related enhancements for automated theorem-proving programs
• Title not available (Why is that?)
• A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains
• Meeting the challenge of fifty years of logic
• Title not available (Why is that?)
• Condensed detachment as a rule of inference

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

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)