### Automated Theorem-Proving for Theories with Simplifiers Commutativity, and AssociativityAutomated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity

Access Restriction
Subscribed

 Author Slagle, James R. Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Copyright Year ©1974 Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science Abstract To prove really difficult theorems, resolution principle programs need to make better inferences and to make them faster. An approach is presented for taking advantage of the structure of some special theories. These are theories with simplifiers, commutativity, and associativity, which are valuable concepts to build in, since they so frequently occur in important theories, for example, number theory (plus and times) and set theory (union and intersection). The object of the approach is to build in such concepts in a (refutation) complete, valid, efficient (in time) manner by means of a “natural” notation and/or new inference rules. Some of the many simplifiers that can be built in are axioms for (left and right) identities, inverses, and multiplication by zero.As for results, commutativity is built in by a straightforward modification to the unification (matching) algorithm. The results for simplifiers and associativity are more complicated. These theoretical results can be combined with one another and/or extended to either $\textit{C}-linear$ refutation completeness or theories with partial ordering, total ordering, or sets. How these results can serve as the basis of practical computer programs is discussed. ISSN 00045411 Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 1974-10-01 Publisher Place New York e-ISSN 1557735X Journal Journal of the ACM (JACM) Volume Number 21 Issue Number 4 Page Count 21 Starting Page 622 Ending Page 642

#### Open content in new tab

Source: ACM Digital Library