|
 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.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
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.
|
| |
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.
|
 |
3
|
|
| |
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.
|
| |
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.
|
| |
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.
|
| |
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.
|
| |
8
|
|
| |
9
|
SLAGLE, J. Artificial intelligence: The Heuristic Programming Approach. McGraw-Hill, New York, 1971. (Also available in Japanese and German translations.)
|
| |
10
|
|
| |
11
|
|
| |
12
|
|
| |
13
|
Wos, L., ChRSON, D., AND ROBINSON, G. The unit preference strategy in theorem proving. Proc. AFIPS 1964 FJCC, Vol. 26, pp. 615-621.
|
| |
14
|
|
| |
15
|
|
CITED BY 38
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Sergio Antoy , Rachid Echahed , Michael Hanus, A needed narrowing strategy, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-279, January 16-19, 1994, Portland, Oregon, United States
|
|
|
|
|
|
|
|
|
Sergio Antoy , Bart Massey , Michael Hanus , Frank Steiner, An implementation of narrowing strategies, Proceedings of the 3rd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.207-217, September 05-07, 2001, Florence, Italy
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
K. Blasius , N. Fisinger , J. Siekmann , G. Smolka , A. Herold , C. Walther, The Markgraf Karl refutation procedure, Proceedings of the 7th international joint conference on Artificial intelligence, p.511-518, August 24-28, 1981, Vancouver, BC, Canada
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
I.2