James R. Slagle
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 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.
- 1 ALLEN, J., AND LUCKHAM, D. An interactive theorem-proving program. In Machine Intelligence 5, B. Me|tzer and D. Michie, Eds., American Elsevier, New York, 1970, pp. 321-336.Google Scholar
- 2 DARLINGTON, J. Automatic theorem proving with equality substitutions and mathematical induction. In Machine Intelligence $, D. Michie, Ed.,Oliver and Boyd, Edinburgh, 1968, pp. 113-127.Google Scholar
- 3 GUARD, J., OGLESBY, F., BENNETT, J., AND SETTLE, L. Semi-automated mathematics. J. ACM 16, 1 (Jan. 1969), 49-62. Google Scholar
- 4 KOWALSKI, R., AND HAYES, P. Semantic trees in automatic theorem-proving. In Machine Intelligence 5, B. Meltzer and D. Michie, Eds., American Elsevier, New York, 1969, pp. 87-101.Google Scholar
- 5 PLOTKIN, G. Building in equational theories. In Machine Intelligence 7, B. Meltzer and D. Michie, Eds., Halsted Press, New York, 1973, pp. 73-90.Google Scholar
- 6 ROBINSON, G., AND WOS, L. Paramodulation and theorem-proving in first order theories with equality. In Machine Intelligence $, B. Meltzer and D. Michie, Eds., American Elsevier, New York, 1969, pp. 135-150.Google Scholar
- 7 ROmNSON, J.A. A review of automatic theorem proving. Proc. Symposia in Applied Mathematics, Vol. 19, Amer. Math. Soc., Providence, R.I., 1967, pp. 1-18.Google Scholar
- 8 SLAGLE, J. An approach for finding C-linear complete inference systems. J. ACM 19, 3 (July 1972), 496-516. Google Scholar
- 9 SLAGLE, J. Artificial intelligence: The Heuristic Programming Approach. McGraw-Hill, New York, 1971. (Also available in Japanese and German translations.)Google Scholar
- 10 SLAGLE, J. Automatic theorem proving with built-in theories including equality, partial ordering, and sets. J. ACM 19, 1 (Jan. 1972), 120-135. Google Scholar
- 11 SLAGLE, J., AND NORTON, L. Automated theorem-proving for the theories of partial and total ordering. Computer J. (to appear). Google Scholar
- 12 SLAGLE, J., AND NORTON, L. Experiments with an automatic theorem-prover having partial ordering inference rules. Comm. ACM 16, 11 (Nov. 1973), 682-688. Google Scholar
- 13 Wos, L., ChRSON, D., AND ROBINSON, G. The unit preference strategy in theorem proving. Proc. AFIPS 1964 FJCC, Vol. 26, pp. 615-621.Google Scholar
- 14 Wos, L., ROBINSON, G., AND CARSON, D. Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12, 4 (Oct. 1965), 536-541. Google Scholar
- 15 Wos, L., ROBINSON, G., CARSON, D., AND SHALLA, L. The concept of demodulation in theorem proving. J. ACM 15, 4 (Oct. 1967), 698-709. Google Scholar
Index Terms
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
Recommendations
Theorem Proving Modulo
AbstractDeduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated theorem proving, is of general interest because it permits one to separate ...
Representation theorems and the semantics of non-classical logics, and applications to automated theorem proving
Beyond twoWe give a uniform presentation of representation and decidability results related to the Kripke-style semantics of several non-classical logics. We show that a general representation theorem (which has as particular instances the representation theorems ...
Discrete lawvere theories
CALCO'05: Proceedings of the First international conference on Algebra and Coalgebra in Computer ScienceWe introduce the notion of discrete countable Lawvere V-theory and study constructions that may be made on it. The notion of discrete countable Lawvere V-theory extends that of ordinary countable Lawvere theory by allowing the homsets of an ordinary ...
Comments