|
 ABSTRACT
The resolution principle is an inference rule for quantifier-free first-order predicate calculus. In the past, the completeness theorems for resolution and its refinements have been stated and proved for finite sets of clauses. It is easy (by Gödel's Compactness Theorem) and of practical interest to extend them to countable sets, thus allowing schemata representing denumerably many axioms. In addition, some theorems similar to Craig's Interpolation Theorem are proved for deduction by resolution. In propositional calculus, the theorem proved is stronger, whereas in predicate calculus the theorems proved are in some ways stronger and in some ways weaker than Craig's theorem. These interpolation theorems suggest procedures which could be embodied in computer programs for automatic proof finding and consequence finding.
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
|
BETH, EVERT W. On Padoa's method in the theory of definition. Koninkl. Ned. Akad. Wetcnsehap. (Amsterdam) Proc.{A}, 56 (1953), 330--339.
|
| |
2
|
CRAIG, WILLIAM. Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symbolic Logic 22 (1957), 250--268.
|
| |
3
|
--.. Three uses of the Herbrand-Gentzen theorem relating model theorem to proof theorem. J. Symbolic Logic 22 (1957), 269-285.
|
| |
4
|
DARLINGTON, JARED L. Automatic theorem proving with equality substitutions and mathematical induction. In Machine Intelligence, Vol. 3, Michie, D. (Ed.), Oliver and Boyd, Edinburgh, 1968, 113-127.
|
| |
5
|
GODEL, KURT. Die Vollstandigbert der Axiome des Logischen Vunktionen Kalkuls. Monatsh. Math. Phys. 87 (1930), 349-360. (Eng. transl, in Ref. {20}.)
|
 |
6
|
|
| |
7
|
GUARD, J. The arbitrarily-large entities in man-machine mathematics. In Formal Systems and Non-numerical Problem Solving by Computers, Mesarovic, Mihajlo D., and Banerji, Ranan B. (Eds.) (in press).
|
| |
8
|
KLEENE, STEPHEN COLE. Ma~-hematical Logic. Wiley, New York, 1967.
|
| |
9
|
|
| |
10
|
MELTZER, BERNARD. Theorem proving for computers: Some results on resolution and renaming. Computer J. 8 (1966), 341-343.
|
| |
11
|
ROBINSON, ABRAHAM. A result on consistency and its application to the theory of definition. Koninkl. Ned. Akad. Wetenschap. (Amsterdam) Proc. {A}, 59 (1956), 47-58.
|
| |
12
|
ROBINSON, GEO~OE, AND Wos, LAWRENCE. Paramodulation and theorem proving in first order series with equality. In Machine Intelligence, Vol. 5, Meltzer, B., and Michie, D. (Eds.), American Elsevier, New York, 1968, pp. 135--150.
|
| |
13
|
|
| |
14
|
Automatic deduction with hyper-resolution. Internat. J. of Computer Math. I (1965), 227-234.
|
| |
15
|
A review of automatic theorem-proving. In Proc. Symposia in Appl. Math. (1966), Vol. 19, Amer. Math. Soc., Providence, R. I., 1967, pp. 1-18.
|
| |
16
|
--. Present state of mathematical theorem proving. In Formal Systems and Nonnumerical Problem Solving by Computers, Mesarovic, Mihajlo D., and Banerji, Ranan B. (Eds.) (in press).
|
| |
17
|
|
| |
18
|
--. Heuristics search program. In Formal Systems and Non-numerical Problem Solving by Computers, Mesarovic, Mihajlo D., and Banerji, Ranan B. (Eds.) (in press).
|
| |
19
|
, CHANG, C. L., AND LEE, R. C.W. Completeness theorems for semantic resolution for consequence-finding. Div. of Computer Res. and Technol., National Institutes of Health, Bethesda, Md., 1969.
|
| |
20
|
VAN HEIJENOORT, JEAN (Ed.). From Frege to GSdel, a Source Book in Mathematical Logic, 1879-1931. Harvard U. Prep., Cambridge, Mass., 1967.
|
| |
21
|
Wos, LAWRENCE, CARSON, DANIEL, AND ROBINSON, G. The unit preference strategy in theorem proving. Proc. AFIPS 1964 Fall Joint Comp. Conf., Vol. 26, Pt. 1, pp. 615-621 (Spartan Books, Baltimore, Md.).
|
| |
22
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
I.2