|
 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
|
|
| |
2
|
BLEDSOE, W. W. Sphtting and reduction heuristics in automatic theorem-proving Arllf . Intel 2 (1971), 55-77
|
| |
3
|
BLEDSOE, W W., BOYER, R. S , AND HENNEMAN, W H Computer proofs of limit theorems. Artlf. Inlel3 (1972), 27-60
|
| |
4
|
BLEDSOE, W W., AND BRUELL, P. A man-machine theorem-proving system. Third International Joint Conf on Artificial Intelligence, 1973, pp. 36-65.
|
| |
5
|
BOYER, R. S., AND MOORE, J S. The sharing of structure in theorem-proving programs. In Machine Intelligence 7, B. Meltzer and D Mmhie, Eds., Edinburgh U. Press, Edinburgh, Scotland, 1972, pp. 101-116
|
| |
6
|
COLMERAUER, A. Lessystemes-Q ou un formahsme pour analyser et synthetiser des phrases sur ordinateur Pub. interne No 43, Dep d'Informatique, Universit6 de Montrdal, Montr6al, Canada, 1970.
|
| |
7
|
COLMERAUER, A Cancellation systems Personal communication, 1972.
|
| |
8
|
COLMERAUER, A., IANOUI, H., PASERO, R , AND ROUSSEL, P. Un systeme de communicationine homme-machgine en Francais. Rapport prehminaire, Groupe de Researche en Intelligence Artificielle, Umvermt d'Alx Marseflle, Luminy, 1972.
|
| |
9
|
EMDEN, M H van. First-order predicate logic as a high-level program language. Memo No. MIP-R-106, U. of Edinburgh, Edinburgh, Scotland, 1974.
|
| |
10
|
GELPERIN, D Deletion-directed search in resolution-based proof procedures Advance Papers of the Third International Joint Conf on Artificial Intelligence, Stanford U., Stanford, Calif., 1973, pp 47-50.
|
| |
11
|
GEOFFRION, A M., AND MARSTEN, R. E Integer programming algorithms' A framework and state-of-the-art survey. Manag. Sci. 18 (1972), 465-491.
|
| |
12
|
HAYES, P. J Computation and deduction. Proc. 2ad MFCS Symposium, Czechoslovak Academy of Sciences, 1973, pp. 105..-118.
|
| |
13
|
HEWlTT, C. PLANNER' A language for proving theorems in robots. Proc of the International Joint Conf. on Artificial Intelligence, Washington D. C , 1969, pp 295--301.
|
| |
14
|
KOWALSKI, R , AND HAYES, P .J . Semantic trees in automatic theorem-proving. In Machine Intelhgence 4, B. Meltzer and D. Michm, Eds, Edinburgh U. Press, Edinburgh, Scotland, 1968, pp. 87-101.
|
| |
15
|
KOWALSKI, R. The case for using equality axioms in automatic demonstration. Proc. IRIA Symposium on Automatic Demonstration (Lecture Notes in Mathematics, No. 125), Sprmger- Verlag, Berlin, Heidelberg, New York, 1968, pp. 112-127.
|
| |
16
|
KOWALSKI, R. Studies in the completeness and efficiency of theorem-proving by resolution. Ph.D Th., U. of Edinburgh, Edinburgh, Scotland, 1970.
|
| |
17
|
KOWALSKI, R. And-or graphs, theorem-proving graphs and bi-dlrectional search In Machine Intell, gence 7, B Meltzer and D Michie, Eds., Edinburgh U Press, Edinburgh, Scotland, 1972, pp 167-194.
|
| |
18
|
iKOWALSKI, R An improved theorem-proving system for first-order logic D C.L. Memo No. 65, U of Edinburgh, Edinburgh, Scotland, 1973.
|
| |
19
|
KOWALSKI, R Predicate logic as programming language. Proc IFIP Cong. 1974, Stockholm, North-Holland Pub. Co, Amsterdam, pp. 569-574.
|
| |
20
|
|
| |
21
|
KOWALSKi, R., AND KUEHNEB, D. Linear resolution with selection function. Artf. lntel 2 (1971), 227-260.
|
| |
22
|
LOVELAND, D. Allnear format for resolution Proc. IRIA Syrup on Automatic Demonstration, Versailles, France, Springer-Verlag, Berlin, Heidelberg, New York, 1970, pp. 147-162.
|
| |
23
|
LUCKHAM, D. Some tree-paring strategies for theorem-proving. In Machzne Intelligence 8, D Mlchm, E d , Edinburgh U Press, Edinburgh, Scotland, 1968, pp. 95-112.
|
| |
24
|
LUCKtiAM, D Refinement theorems in resolution theory. Proc. IRIA Symp on Automatic Demonstration, Versailles, France, Springer-Verlag, Berlin, Heidelberg, New York, 1970, pp. 162-190
|
| |
25
|
MELTZER, B. Some notes on resolution strategies. In Machzne lntellzgenee 8, D. Michie, E d , Edinburgh U. Press, Edinburgh, Scotland, 1968, pp 71-75
|
| |
26
|
MINKER, J , AND VAN DER BRUG, G. J Representations of the language recognition problem for a theorem-prover. Tech. Rep. TR-199, Computer Science Center, U of Maryland, College Park, Md., 1972.
|
| |
27
|
|
| |
28
|
PORL, I. Bi-directional search. In Machine Intelligence 7, B. Meltzer and D. Michie, Eds., Edinburgh U. Press, Edinburgh, Scotland, 1972, pp 127-140.
|
| |
29
|
|
| |
30
|
|
| |
31
|
ROBINSON, J. A. Automatic deduction with hyper-resolution. Int. J. of Computer Math. 1 (1965), 227-234.
|
| |
32
|
ROBINSON, J A A review of automatic theorem-proving Proc. of Symposia in Applied Mathematics, Vol 19, Amer. Math. Soc , Prowdence, R. I., 1967, pp. 1-18
|
| |
33
|
|
| |
34
|
WILKINS, D E. QUEST. A non-clausal theorem-proving system. M.Se. T h , U of Essex, Colhester, Essex, England, 1973.
|
| |
35
|
WINSTON, P. H The M I T Robot. In Machine Intelligence 7, B. Meltzer and D. Mlchie, Eds., Edinburgh U. Press, Edinburgh, Scotland, 1972, pp 431--463
|
| |
36
|
WoN, L., CARSON, D. F , AND ROBINSON, G A The unit preference strategy in theoremproving Proc. AFIPS 1964 FJCC, Vol 26, Spartan Books, New York, pp 616-621.
|
| |
37
|
|
| |
38
|
ZAMOV, N K , AND SHARONOV, V I. On a class of strategies which can be used to establish decidability by the resolution principle (In Russian). Issled po konstruktivnoye matematkye i matematchesko,e logkye 111 16 (1969), 54-64 (National Lending Library, Russian Translating Program 5857, Boston Spa, Yorkshire), England)
|
CITED BY 47
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Charles Kellogg , Philip Klahr , Larry Travis, A deductive capability for data management, Proceedings of the second international conference on Systems for Large Data Bases, p.181-196, September 08-10, 1976, Brussels, Belgium, North Holland
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Richard Whitney , Darrel J. VanBuer , Donald P. McKay , Dan Kogan , Lynette Hirschman , Rebecca Davis, A predicate connection graph based logic with flexible control, Proceedings of the 9th international joint conference on Artificial intelligence, p.733-736, August 18-23, 1985, Los Angeles, California
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
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
G.2