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-7zbMATH Open0553.68051OpenAlexW2074713171WikidataQ114262293 ScholiaQ114262293MaRDI QIDQ759491FDOQ759491
Authors: 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
Recommendations
- Shortest single axioms for the equivalential calculus with CD and RCD
- Searching for circles of pure proofs
- scientific article; zbMATH DE number 3904002
- scientific article; zbMATH DE number 3952747
- A finitely axiomatized formalization of predicate calculus with equality
- scientific article; zbMATH DE number 4049134
- The laws of Occam programming
- Remarks on Dudek's E-groupoids
- Automated reasoning contributes to mathematics and logic
- RETRPROV. A system that looks for axioms
automated reasoningAURAequivalential calculusever-increasing length conjecture of deducible formulasshortest single axiom property
Other nonclassical logic (03B60) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)
Cites Work
- Title not available (Why is that?)
- A Machine-Oriented Logic Based on the Resolution Principle
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A shortest single axiom for the classical equivalential calculus
- Notes on the axiomatics of the propositional calculus
- Title not available (Why is that?)
- Title not available (Why is that?)
- Complexity and related enhancements for automated theorem-proving programs
- The Concept of Demodulation in Theorem Proving
- 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
- An automatic theorem prover for substitution and detachment systems
- Semigroups, Antiautomorphisms, and Involutions: A Computer Solution to an Open Problem, I
- Title not available (Why is that?)
- 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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Axiomatizations of Logics with Values in Groups
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (11)
- Towards finding longer proofs
- Title not available (Why is that?)
- The problem of selecting an approach based on prior success
- Automated reasoning contributes to mathematics and logic
- Meeting the challenge of fifty years of logic
- Problems on the generation of finite models
- Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus
- The application of automated reasoning to questions in mathematics and logic
- Searching for circles of pure proofs
- A case study in automated theorem proving: Finding sages in combinatory logic
- The problem of choosing the type of subsumption to use
Uses Software
This page was built for publication: A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q759491)
