Unnecessary inferences in associative-commutative completion procedures
- 1 December 1990
- journal article
- research article
- Published by Springer Nature in Theory of Computing Systems
- Vol. 23 (1) , 175-206
- https://doi.org/10.1007/bf02090774
Abstract
No abstract availableKeywords
This publication has 23 references indexed in Scilit:
- RRL: A rewrite rule laboratoryPublished by Springer Nature ,2005
- An equational approach to theorem proving in first-order predicate calculusACM SIGSOFT Software Engineering Notes, 1985
- A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithmACM SIGSAM Bulletin, 1983
- A Unification Algorithm for Associative-Commutative FunctionsJournal of the ACM, 1981
- Complete Sets of Reductions for Some Equational TheoriesJournal of the ACM, 1981
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting SystemsJournal of the ACM, 1980
- Non-resolution theorem provingArtificial Intelligence, 1977
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and AssociativityJournal of the ACM, 1974
- Paramodulation and set of supportPublished by Springer Nature ,1970
- Structure Theory for Algebraic Algebras of Bounded DegreeAnnals of Mathematics, 1945