Robert Kowalski
- 1 ANDREWS, P B. Resolution with merging. J ACM 15, 3 (July 1968), 367-381. Google Scholar
- 2 BLEDSOE, W. W. Sphtting and reduction heuristics in automatic theorem-proving Arllf . Intel 2 (1971), 55-77Google Scholar
- 3 BLEDSOE, W W., BOYER, R. S , AND HENNEMAN, W H Computer proofs of limit theorems. Artlf. Inlel3 (1972), 27-60Google Scholar
- 4 BLEDSOE, W W., AND BRUELL, P. A man-machine theorem-proving system. Third International Joint Conf on Artificial Intelligence, 1973, pp. 36-65.Google Scholar
- 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-116Google Scholar
- 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.Google Scholar
- 7 COLMERAUER, A Cancellation systems Personal communication, 1972.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 12 HAYES, P. J Computation and deduction. Proc. 2ad MFCS Symposium, Czechoslovak Academy of Sciences, 1973, pp. 105.-118.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 16 KOWALSKI, R. Studies in the completeness and efficiency of theorem-proving by resolution. Ph.D Th., U. of Edinburgh, Edinburgh, Scotland, 1970.Google Scholar
- 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.Google Scholar
- 18 iKOWALSKI, R An improved theorem-proving system for first-order logic D C.L. Memo No. 65, U of Edinburgh, Edinburgh, Scotland, 1973.Google Scholar
- 19 KOWALSKI, R Predicate logic as programming language. Proc IFIP Cong. 1974, Stockholm, North-Holland Pub. Co, Amsterdam, pp. 569-574.Google Scholar
- 20 KOWALSKX, R Logic for problem-solving D.C L. Memo No. 75, U. of Edinburgh, Edinburgh, Scotland, 1974 Google Scholar
- 21 KOWALSKi, R., AND KUEHNEB, D. Linear resolution with selection function. Artf. lntel 2 (1971), 227-260.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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-190Google Scholar
- 25 MELTZER, B. Some notes on resolution strategies. In Machzne lntellzgenee 8, D. Michie, E d , Edinburgh U. Press, Edinburgh, Scotland, 1968, pp 71-75Google Scholar
- 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.Google Scholar
- 27 NILSSON, N .J . Problem solving methods in artificial intelligence. McGraw-Hill, New York, 1971 Google Scholar
- 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.Google Scholar
- 29 REITER, R. The predicate elimination strategy in theorem-proving Proe. 2nd ACM Symp on the Theory of Computing, Northampton, Mass, 1970, pp 180-183. Google Scholar
- 30 ROBINSON, J. A. A machine-oriented logic based on the resolution principle J. ACM 12, 1 (Jan 1965), 23-41 Google Scholar
- 31 ROBINSON, J. A. Automatic deduction with hyper-resolution. Int. J. of Computer Math. 1 (1965), 227-234.Google Scholar
- 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-18Google Scholar
- 33 STILLMAN, R. B The concept of weak substitution in theorem-proving. J ACM 20, 4 (Oct. 1973), 648-667. Google Scholar
- 34 WILKINS, D E. QUEST. A non-clausal theorem-proving system. M.Se. T h , U of Essex, Colhester, Essex, England, 1973.Google Scholar
- 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--463Google Scholar
- 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.Google Scholar
- 37 WoN, L., ROBINSON, G A, AND CARSON, D. F Efficiency and completeness of the set of support strategy in theorem proving J ACM 12, 4 (Oct 1965), 536-541. Google Scholar
- 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)Google Scholar
Index Terms
- A Proof Procedure Using Connection Graphs
Recommendations
Monochromatic k-edge-connection colorings of graphs
AbstractA path in an edge-colored graph G is called monochromatic if any two edges on the path have the same color. For k ≥ 2, an edge-colored graph G is said to be monochromatic k-edge-connected if every two distinct vertices of G are ...
Rainbow connection in oriented graphs
An edge-coloured graph G is said to be rainbow-connected if any two vertices are connected by a path whose edges have different colours. The rainbow connection number of a graph is the minimum number of colours needed to make the graph rainbow-...
Rainbow Connection in Graphs with Minimum Degree Three
Combinatorial AlgorithmsAn edge-coloured graph G is rainbow connected if any two vertices are connected by a path whose edges have distinct colours. The rainbow connection number of a connected graph G , denoted rc ( G ), is the smallest number of colours that are ...
Comments