Refutational theorem proving using term-rewriting systems
- 31 March 1985
- journal article
- Published by Elsevier in Artificial Intelligence
- Vol. 25 (3), 255-300
- https://doi.org/10.1016/0004-3702(85)90074-8
Abstract
No abstract availableKeywords
This publication has 13 references indexed in Scilit:
- Orderings for term-rewriting systemsTheoretical Computer Science, 1982
- A simplified problem reduction formatArtificial Intelligence, 1982
- A complete proof of correctness of the Knuth-Bendix completion algorithmJournal of Computer and System Sciences, 1981
- Complete Sets of Reductions for Some Equational TheoriesJournal of the ACM, 1981
- A Catalogue of Canonical Term Rewriting Systems.Published by Defense Technical Information Center (DTIC) ,1980
- Non-resolution theorem provingArtificial Intelligence, 1977
- Proving Theorems with the Modification MethodSIAM Journal on Computing, 1975
- Experiment with an automatic theorem-prover having partial ordering inference rulesCommunications of the ACM, 1973
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965
- Theorem-Proving on the ComputerJournal of the ACM, 1963