Logic and logic programming

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Logic and logic programming

Full text

Pdf (6.56 MB)

Source

Communications of the ACM archive
Volume 35 , Issue 3 (March 1992) table of contents

Pages: 40 - 65

Year of Publication: 1992

ISSN:0001-0782

Author

J. A. Robinson

Office of the University Professor, Syracuse University, Syracuse, NY

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 67, Citation Count: 5

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/131295.131296 What is a DOI?

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	Krzysztof R. Apt , M. H. van Emden, Contributions to the Theory of Logic Programming, Journal of the ACM (JACM), v.29 n.3, p.841-862, July 1982 [doi>10.1145/322326.322339]
	2	Barktumt, J., Parallel unification, Ph.D. thesis, Computing Science Department, Uppsala Univertsity, 1990,.
	3	Baxter, L.D. An efficient unification algorithm. Tech. Rep. CS-73- 23, Department of Computer Science, University of Waterloo, 1973.
	4	Lewis Denver Baxter, The complexity of unification., 1976
	5	Boyer, R.S., and Moore, J.S., The Sharing of Structure in Theorem Proving Programs. Math. Intell. 7 1972), 101-116.
	6	Church, A. A note on the entcheidungs problem. J. Symbolic Logic I (1936).
	7	Colmerauer. A. Les Systemes-Q ou un formalisme pour analyser et synthesizer des phrases sur ordinateur. Rep. 43, Department of Computer Science, University of Montreal, 1970.
	8	Colmerauer, A., Kanoui, H., Pasero, R. and Roussel, P. Un systeme de communication hommemachine en Francais. Tech. Rep., Groupe d'Intelligence Artificille, Universite d'Aix Marselle II, Luminy, France, 1973,
	9	Davidon, W. Personal communication, 1962.
	10	Davis, M. Eliminating the irrelevant from mechanical proofs. In Proceedings, Symposix of Applied Mathematics 15, American Mathematical Society, 1963, pp. 15-30. (Reprinted in (44), vol. 1, 315-330).
	11	Martin Davis, The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Dover Publications, Incorporated, 2004
	12	Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
	13	Cynthia Dwork , Paris C. Kanellakis , John C. Mitchell, On the sequential nature of unification, Journal of Logic Programming, v.1 n.1, p.35-50, June 1984 [doi>10.1016/0743-1066(84)90022-0]
	14	Frege, G. Begriffsschrifft, a Formula Language, Modelled Upon that of Arithmetic, for Pure Thourght, English translation in (48), 1-82.
	15	Gentzen, G. The Collected Papers of Gerhard Genturn. M.E., Szabo Ed., North-Holland, 1969,
	16	Gilmore, P.C. A Proof Method for Quantification Theory: its Justification and Realzation. IBM J. Res. Dew 4 (1960), 28-35, (Reprinted in {44}, volume 1, 151-158.
	17	Godel, R. The Completnes of the Axioms of the Functional Calculus of Logic, 1930. English tranlsation, with commentary, in {48}, 582-291.
	18	Green, C.C. The application of theorem-proving to problem solving. In proceedings of the first International Joint Conference on Artificial Intelligence (Washington: D,C., 1969), p.p. 219-240,
	19	Herbrand, J. Investigation in Proof Theory (1930). English translation of main parts: with: commentary, in {48}, 525-581, and of entire thesis in Jacques Herbraud: Logical Writings (edited by Warren Goldfarb), Harvard, 1971, 44-202.
	20	Hewitt, C. PLANNER: A lanffuage for proving theorems in robots. In Proceedings of the first International joint Conference on Artificial Intelligence, (Wash., D.C., 1969), pp. 295-301.
	21	Hill, R. LUSH Resolution and its Completeness. DCL Mem. 78, Department of Artificial Intelligence, University of Edinburgh, 1974.
	22	Huet, G. Resolution des equations dam tangages d'order 1, 2 .... co. These d'Etat, Universite Paris VII, 1976.
	23	Kneale, W.C. and Kneale, M. The Development of Logic. Oxford, 1962.
	24	Kowalski, R.A. Predicate Calculus as a Programming Language. In Proceedings of Sixth IFIP Congress, North Holland, 1974 pp.569-574.
	25	Robert Kowalski, Logic for problem-solving, North-Holland Publishing Co., Amsterdam, The Netherlands, 1986
	26	Robert A. Kowalski, The early years of logic programming, Communications of the ACM, v.31 n.1, p.38-43, Jan. 1988 [doi>10.1145/35043.35046]
	27	Kowalski, R.A. and Kuehenr d.- Linear Resolution with Selection Function. Artificial Intelligence 2 (1971), 227-260. (Reprinted in {44}, volume 1, 542-577).
	28	Donald W. Loveland, Mechanical Theorem-Proving by Model Elimination, Journal of the ACM (JACM), v.15 n.2, p.236-251, April 1968 [doi>10.1145/321450.321456]
	29	L6wenheim, L. On Possibilities in the Caicui~ of Relatives, i9 i5. English translation in {48}, 228-251.
	30	Luckham, D. Refinement Theorems in Resolution Theory. Lecture Notes in Mathematics 125, Springer, 1970, 163-190.
	31	McCarthy, j. Programs with Common Sense. In Proceedings of a S?nposium on the Mechanization oJ Thought H.M. Stationery Office, London, 1959. (Reprinted in Semantic Information Processing MIT Press, 1968).
	32	Marvin Minsky, The society of mind, Simon & Schuster, Inc., New York, NY, 1986
	33	Newell, A., Empirical explorations with the logic theory machine- A case the Western Joint Computer Conference (1957), pp. 218-239. (Reprinted in
	34	Prawitz, D. An Improved Proof Procedure. Theo~a 26 (1960) 102-139. (Reprinted in {44}, volume !, !59- 199, with a preface by the author).
	35	Dag Prawitz , Haå kan Prawitz , Neri Voghera, A Mechanical Proof Procedure and its Realization in an Electronic Computer, Journal of the ACM (JACM), v.7 n.2, p.102-128, April 1960 [doi>10.1145/321021.321023]
	36	Raphael, B. Programming a robot. gress, North Holland, 1968, 135- I39.
	37	Done by Man, Logician, or Machine). Summaries of talks presented at the Summer Institute for Symbolic Logic. Communications Research Division, Institute for Defense Analysis, Princeton, 1957. (Reprinted in {44}, volume 1, 74- 76).
	38	J. A. Robinson, Theorem-Proving on the Computer, Journal of the ACM (JACM), v.10 n.2, p.163-174, April 1963 [doi>10.1145/321160.321166]
	39	J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
	40	Robinson, J.A. Automatic Deduc- Comput. Math. I (1965), 227-234. (Reprinted in {44}, volume 1,416-
	41	Robinson, J.A. Computational logic: the unification computation. Machine Intell. 6 (1970), 63-72.
	42	Robinson, J.A. Fast Unification. Tagung fiber Automatisches Beweisen, Mathematics Forschungsinstitut Oberwolfach, 1976.
	43	Robinson, G.A. and Wos, L.~ Paramodulation and theorem proving in first-order theories with equality. Machine intell. 4 (1969), 103-133.
	44	Siekmann, J.H. and Wrightson, G. Eds. Automation of Reasoning. Classical Papers on Computational Logic (1957-1966). Two volumes,
	45	Skolem, T. Logico-combinatorial Investigations in the Satisfmbility or t/ons (1920). English translation, with commentary, in {48}, 252-263.
	46	Tarski, A. Logic, Semantics Metamathematics: Papers from 1923 to 1938, translated by J.H. Woodger, Oxford 1956.
	47	Turing, A.M. On computable numbers, with an application to the entscheidungsproblem. In Proceedings of the London Mathematical Society, 1937. (Reprinted in {11}).
	48	van Heijenoort, j. Ed. From Frege to Godet; A Source Book in Mathematical Logic, 1879-1931. Harvard Univer-
	49	Wang, H. Towards mechanical mathematics. IBM J. Res. Dev. 4 volume 1, 244-264).
	50	Warren, D.H.D. Implementing PROLOG--compiling predicate logic programs (Res. Rep. 39 and 40), and Logic programming and Department of Artificial Intelligence, University of Edinburgh,
	51	Terry Winograd, Understanding Natural Language, Academic Press, Inc., Orlando, FL, 1972
	52	Wos, L.T., Carson, D. and Robinson, G.A. The unit preference strategy in theorem proving. AFIPS Conference Proceedings 26, Spartan Books, Wash. D.C., 1964, pp. 615- 621. (Reprinted in {44}, vol. 1,387-
	53	Lawrence Wos , George A. Robinson , Daniel F. Carson, Efficiency and Completeness of the Set of Support Strategy in Theorem Proving, Journal of the ACM (JACM), v.12 n.4, p.536-541, Oct. 1965 [doi>10.1145/321296.321302]
	54	J.W.Llloyd's Foundations of Logic Programming (second, extended edition, Springer-Veriag i987) and Logic, Programming and Proiog by Ulf Nilsson and Jan Maluszynski (Wiley, i990)
	55	The Art of Prolog by L. Sterling and E. Shapiro (MIT Press, i986);
	56	Ivan Bratko, PROLOG Programming for Artificial Intelligence, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
	57	Richard A. O'Keefe, The craft of Prolog, MIT Press, Cambridge, MA, 1990
	58	Christopher John Hogger, Essentials of logic programming, Oxford University Press, Inc., New York, NY, 1990
	59	Franz Kurfeb, Parallelism in Logic: Its Potential for Performance and Program Development, Informatica International, Incorporated, 1991
	60	Parallel Logic Programming by Evan Tick (MIT Press, 1991).

CITED BY 5

	John Grant , Jack Minker, The impact of logic programming on databases, Communications of the ACM, v.35 n.3, p.66-81, March 1992
	Eberhard U. Stickel, A linear programming approach to logical inference, Proceedings of the 1993 ACM conference on Computer science, p.100-106, February 16-18, 1993, Indianapolis, Indiana, United States
	Donald MacKenzie, The Automation of Proof: A Historical and Sociological Exploration, IEEE Annals of the History of Computing, v.17 n.3, p.7-29, September 1995
	Cliff B. Jones, The Early Search for Tractable Ways of Reasoning about Programs, IEEE Annals of the History of Computing, v.25 n.2, p.26-49, April 2003
	Selmer Bringsjord , David A. Ferrucci, Logic and Artificial Intelligence: Divorced, Still Married, Separated...?, Minds and Machines, v.8 n.2, p.273-308, November 1998