A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering that x 3 = x Implies Ring Commutativity
- 1 January 1984
- book chapter
- Published by Springer Nature
Abstract
No abstract availableKeywords
This publication has 8 references indexed in Scilit:
- A complete proof of correctness of the Knuth-Bendix completion algorithmJournal of Computer and System Sciences, 1981
- A Unification Algorithm for Associative-Commutative FunctionsJournal of the ACM, 1981
- Complete Sets of Reductions for Some Equational TheoriesJournal of the ACM, 1981
- Canonicalization and demodulationPublished by Office of Scientific and Technical Information (OSTI) ,1981
- Proofs by induction in equational theories with constructorsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1980
- Non-resolution theorem provingArtificial Intelligence, 1977
- Simple Word Problems in Universal Algebras††The work reported in this paper was supported in part by the U.S. Office of Naval Research.Published by Elsevier ,1970
- Structure Theory for Algebraic Algebras of Bounded DegreeAnnals of Mathematics, 1945