|
 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, O. An interactive theorem-proving program. In Machine Intelligence 5, B. Meltzer and D. Michie, Eds., American Elsevier, New York, 1970, pp. 321-336.
|
 |
2
|
|
| |
3
|
|
| |
4
|
G/SDEL, K. Die Vollst~indigkeit der Axiome des logischen Funktionenkalktils. Monatsh. Math. Phys. 37 (1930), 349-360 (English translation in {14, pp. 582-591}).
|
| |
5
|
LOVELAND, D. A linear format for resolution. Symposium on Automatic Demonstration, Lecture Notes in Math. No. 125, M. Lander et al., Eds., Springer-Verlag, Berlin, 1970, pp. 147-162.
|
| |
6
|
LUCKHAM, D. Refinement theories in resolution theory. Symposium on Automatic Demonstration, Lecture Notes in Math. No. 125, M. Laudet et al., Eds., Springer-Verlag, Berlin, 1970, pp. 163-190.
|
| |
7
|
ROBINSON, J. A. Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1 (1965), 227-234.
|
| |
8
|
ROBINSON, J.A. A review of automatic theorem proving. Proc. Symposia in Appl. Math., Vol. 19, J. Schwartz, Ed., Amer. Math. Soc., Providence, R. I., 1967, pp. 1-18.
|
| |
9
|
SLAGLE, J. Artificial Intelligence: The Heuristic Programming Approach. McGraw-Hill, New York, 1971.
|
| |
10
|
|
| |
11
|
|
| |
12
|
SL:~GLF~, J., CHANG, C., AND LEE, R. Completeness theorems for semantic resolution in consequence-finding. Proc. Internat. Joint Conf. on Artificial Intelligence, Walker, D. E., and Norton, L. M., Eds., 1969, pp. 281-285.
|
| |
13
|
|
| |
14
|
VAN HEIJENOORT, J. (Ed.). From Frege to G5del: A Source Book in Mathematical Logic, 1879 1931. Harvard U. Press, Cambridge, Mass., 1967.
|
| |
15
|
Wos, L., CARSON, })., AND ROBINSON, (_~. The unit preference strategy in theorem proving. Proc. AFIPS 1964 FJCC, Vol. 26, Pt. 1, Spartan Books, New York, pp. 615-621.
|
| |
16
|
|
| |
17
|
Wos, L., AND ROBINSON, G. Maximal models and refutation completeDess: Semidecision procedures i_,~ automatic theorem proving. In Word Problems i~ Group Theory: The Burnside Problem and Decisiort Problems, W. W. Boone, F. B. Cannouito, and R. C. Lyndon, Eds., North-Holland Pub. Co., Amsterdam (in press).
|
| |
18
|
WOS, L., AND ROBINSON, G. Paramodulation and set of support. Symposium o~ Automatic Demot~stratiot~, Lecture Notes in Math. No. 125, M. Laudet et al., Eds., Springer-Verlag, Berlin, 1970, pp. 276-310.
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
I.2