Procedure implementation through demodulation and related tricks
- 5 October 2005
- book chapter
- Published by Springer Nature
- p. 109-131
- https://doi.org/10.1007/bfb0000054
Abstract
No abstract availableKeywords
This publication has 10 references indexed in Scilit:
- Canonicalization and demodulationPublished by Office of Scientific and Technical Information (OSTI) ,1981
- 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
- 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
- An implementation of hyper-resolutionComputers & Mathematics with Applications, 1975
- The Concept of Demodulation in Theorem ProvingJournal of the ACM, 1967
- Efficiency and Completeness of the Set of Support Strategy in Theorem ProvingJournal of the ACM, 1965
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965