Arthur J. Nevins
Skip Abstract Section
Abstract
A deductive system is described which combines aspects of resolution (e.g. unification and the use of Skolem functions) with that of natural deduction and whose performance compares favorably with the best predicate calculus theorem provers.
- 1 ALLEN, JOHN, AND LUCKHAM, DAVID. An interactive theorem proving program. In Machine Intelligence 5. B. Meltzer and D. Michie, Eds., Edinburgh. U. Press, Edinburgh, 1970, pp. 321- 336.Google Scholar
- 2 BLEgSOE, W.W. Splitting and reduction heuristics in automatic theorem proving. Artif. Intel. 2 (Spring 1971), 55-77.Google Scholar
- 3 BLEDSOE, W. W., BOYER, ROBERT S., AND HENNEMAN, WILLIAM I~. Computer proofs of limit theorems. Artif. Intel. 3 (Spring 1972), 27-60.Google Scholar
- 4 CHANG, C.L. The unit proof and the input proof in theorem proving. J. ACM 17, 4 (Oct. 1970), 698-707. Google Scholar
- 5 CHANG, C. L. Theorem proving with variable-constrained resolution. Inform. Sciences $, 3 (July 1972), 217-231.Google Scholar
- 6 CHINTHAYAMMA. Sets of independent axioms for a ternary Boolean algebra. Notices Amer. Math. Soc. 16, 4 (June 1969), 69T-A69, 654.Google Scholar
- 7 ERNST, GF~OaGF~ W. The utility of independent subgoals in theorem proving. Inform. and Contr. 18, 3 (April 1971), 237-252.Google Scholar
- 8 KLEENE, STEPHEN C. Introduction to Metamathematics. Van Nostrand, Princeton, N.J., 1952.Google Scholar
- 9 KOWALSKI, ROBERT, AND KUEHNER, DAVID. Linear resolution with selection function. Artif. Intel. 2 (Winter 1971), 227-260.Google Scholar
- 10 LOVELAND, DONALD W. A unifying view of some linear Herbrand procedures. J. ACM 19, 2 (April 1972), 366-384. Google Scholar
- 11 MORRIS, jAMES B. E-resolution: Extension of resolution to include the equality relation. Proc. int. Joint Conf. Artificial Intelligence, Washington, D.C., 1989, pp. 287-294.Google Scholar
- 12 NILSSON, NILE J. Problem Solving Methods in Artificial Intelligence. McGraw-Hill, New York, 1971. Google Scholar
- 13 NORTON, LEWIS M. Experiments with a heuristic theorem-proving program for predicate calculus with equality. Artif. Intel. 2 (Winter 1971), 261-284.Google Scholar
- 14 ROBINSON, GEORGE, AND WOS, LAWRENCE. Paramodulation and theorem-proving in first order theories with equality. In Machine Intelligence 4, B. Meltzer and D. Michie, Eds., Edinburgh U. Press, Edinburgh, 1969, pp. 135-150.Google Scholar
- 15 ROBINSON, JOHN A. Theorem-proving on the computer. J. ACM 10, 2 (April 1963), 163-174. Google Scholar
- 16 ROSlNSON, JoHN A. A machine-oriented logic based on the resolution principle. J. ACM 12, 1 (Jan. 1965), 23-41. Google Scholar
- 17 SHANNON, CLAUDE E., AND WEAVER, WARREN. The Mathematical Theory of Communication. U. of Illinois Press, Urbana, Ill., 1949. Google Scholar
- 18 SLAGLE, JAMES R., AND KONIVER, DEENA A. Finding resolution graphs and using duplicate goals in AND/OR trees. Inform. Sciences 3, 4 (Oct. 1971), 315-342.Google Scholar
- 19 Wos, L~WR~NCE, ROUlNSON, GEORGE A., AND CARSON, DANIEL F. Efficiency and completeness in the set of support strategy in theorem proving. J. ACM I2, 4 (Oct. 1965), 536-541. Google Scholar
Index Terms
- A Human Oriented Logic for Automatic Theorem-Proving
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 ...
Comments