A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains

DOI10.1016/0004-3702(84)90054-7zbMath0553.68051OpenAlexW2074713171WikidataQ114262293 ScholiaQ114262293MaRDI QIDQ759491

D. Kharzeev

Publication date: 1984

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0004-3702(84)90054-7

zbMATH Keywords

automated reasoningAURAequivalential calculusever-increasing length conjecture of deducible formulasshortest single axiom property

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)

Related Items

Towards finding longer proofs, A case study in automated theorem proving: Finding sages in combinatory logic, The application of automated reasoning to questions in mathematics and logic, Searching for circles of pure proofs, Meeting the challenge of fifty years of logic, Problems on the generation of finite models, The problem of selecting an approach based on prior success, The problem of choosing the type of subsumption to use

Uses Software

• AURA

Cites Work

• 6th Conference on Automated Deduction, New York, USA, June 7-9, 1982
• Questions concerning possible shortest single axioms for the equivalential calculus: An application of automated theorem proving to infinite domains
• Shortest single axioms for the classical equivalential calculus
• Complexity and related enhancements for automated theorem-proving programs
• An automatic theorem prover for substitution and detachment systems
• A shortest single axiom for the classical equivalential calculus
• Notes on the axiomatics of the propositional calculus
• Semigroups, Antiautomorphisms, and Involutions: A Computer Solution to an Open Problem, I
• Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions
• Problems and Experiments for and with Automated Theorem-Proving Programs
• Axiomatizations of Logics with Values in Groups
• A Machine-Oriented Logic Based on the Resolution Principle
• The Concept of Demodulation in Theorem Proving
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item