A new use of an automated reasoning assistant: Open questions in equivalential calculus and the study of infinite domains
- 1 April 1984
- journal article
- Published by Elsevier in Artificial Intelligence
- Vol. 22 (3) , 303-356
- https://doi.org/10.1016/0004-3702(84)90054-7
Abstract
No abstract availableKeywords
This publication has 11 references indexed in Scilit:
- Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open QuestionsJournal of the ACM, 1982
- A shortest single axiom for the classical equivalential calculus.Notre Dame Journal of Formal Logic, 1978
- An automatic theorem prover for substitution and detachment systems.Notre Dame Journal of Formal Logic, 1978
- Axiomatizations of Logics with Values in GroupsJournal of the London Mathematical Society, 1976
- Problems and Experiments for and with Automated Theorem-Proving ProgramsIEEE Transactions on Computers, 1976
- Shortest single axioms for the classical equivalential calculus.Notre Dame Journal of Formal Logic, 1976
- Complexity and related enhancements for automated theorem-proving programsComputers & Mathematics with Applications, 1976
- The Concept of Demodulation in Theorem ProvingJournal of the ACM, 1967
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965
- Notes on the axiomatics of the propositional calculus.Notre Dame Journal of Formal Logic, 1963