|
 ABSTRACT
Sentences in first-order predicate logic can be usefully interpreted as programs. In this paper the operational and fixpoint semantics of predicate logic programs are defined, and the connections with the proof theory and model theory of logic are investigated. It is concluded that operational semantics is a part of proof theory and that fixpoint semantics is a special case of model-theoretic semantics.
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
|
BEKIt~, H Definable operations m general algebra, and the theory of automata and flow charts IBM Res Rep , Vienna, 1971
|
| |
2
|
BLEDSOE, W W Splitting and reduction heuristics in automatic theorem proving Arttf Intel 2 (1971), 55-77
|
| |
3
|
BURSTALL, R M Formal description of program structure and semantics in first order toglc. In Machme Intelhgence 5, B Meltzer and D Mtchie, Eds , Edinburgh U Press, Edinburgh, 1969, pp 79-98
|
| |
4
|
CrluRCri, A lntroducuon to Mathemaucal Logic, Vol 1 Princeton U Press, Princeton, N J , 1956
|
| |
5
|
COLMEP, AUWR, A, KANOUI, H , PASERO, R., AND ROUSSEL, P. Un syst~me de communlcatton hommemachine en franqais. Groupe d'Intelhgence Artlficlelle, U E R de Lummy, Umverslt6 d'Aix-Marsedle, Lummy, 1972
|
| |
6
|
DE BAKKER, J W Recursive procedures Tract No 24, Mathematical Centre, Amsterdam, 1971
|
| |
7
|
DE BAKKER, J W, AND DE ROEVER, W P A calculus of recursive program schemes. In Automata, Languages and Programmmg, M Nlvat, Ed , North*Holland Pub Co , Amsterdam, 1973, pp 167- 196
|
| |
8
|
ERNST, G W The utility of independent subgoals tn theorem proving Inform Contr 18, 3 (April 1971), 237-252
|
| |
9
|
KANOUI, H Application de la d6monstration automatlque aux manipulations algebnques et ~ l'mt6gration formelle sur ordmateur Groupe d'Intelhgence Artlficmlle, U E R de Lummy, Umverslt6 d'Aix- Marsellle, Lummy, 1973.
|
| |
10
|
KOWALSKI, R Predicate logic as programming language Proc IFIP Cong 1974, North-Holland Pub Co , Amsterdam, 1974, pp 569-574
|
| |
11
|
KOWALSKI, R Logic for problem-solvmg DCL Memo 75, Dep Artificial Intelligence, U. of Edinburgh, Edmburgh, 1974
|
| |
12
|
KOWALSKI, R , AND KUEHNER, D Lmear resolution with selection function Amf lntel 2 (1971), 227- 260
|
 |
13
|
|
| |
14
|
|
| |
15
|
|
| |
16
|
|
| |
17
|
PARK, D F,xpomt mductton and proofs of program properties In Machme lntelhgence 5, B Meltzer and D Mlchie, Eds, Edmburgh U Press, Edmburgh, 1969, pp 59-78
|
| |
18
|
PAS~RO, R. Repr6sentat~on du fran~a~s en loglque du premier ordre en vue de dlaloguer avec un ordmateur Group d'Intelhgence Artlflclelle, U.E R de Lummy, Umvers~t6 d'A,x-Marsedle, Lummy, 1973.
|
| |
19
|
|
| |
20
|
|
| |
21
|
ROBINSON,J A Automatic deduction with hyper-resolut,on lnt J Comptr Math 1 (1965), 227-234
|
| |
22
|
SCOTT, D Outhne of a mathematical theory of computation Tech Monog PRG-2, Comptg Lab, Oxford U , Oxford, England
|
| |
23
|
SLA~tE, J R , Argo KONtVER, P Finding resolution graphs and using duphcate goals m AND/OR trees Inform Sct 3 (1971),315-342
|
| |
24
|
WARnEN, D H D WARPLAN A system for generattng plans DCL Memo 76, Dep. of Art,fic,al Intelhgence, U of Edinburgh, Edinburgh, 1974
|
CITED BY 190
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
C. Beeri , S. Naqvi , R. Ramakrishnan , O. Shmueli , S. Tsur, Sets and negation in a logic data base language (LDL1), Proceedings of the sixth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.21-37, March 23-25, 1987, San Diego, California, United States
|
|
|
|
|
|
|
|
|
Anna Ciampolini , Evelina Lamma , Paola Mello , Cesare Stefanelli, Abductive coordination for logic agents, Proceedings of the 1999 ACM symposium on Applied computing, p.134-140, February 28-March 02, 1999, San Antonio, Texas, United States
|
|
|
Patrick Cousot , Radhia Cousot, Inductive definitions, semantics and abstract interpretations, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.83-94, January 19-22, 1992, Albuquerque, New Mexico, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
A. Bossi , M. Bugliesi , M. Gabbrielli , G. Levi , M. C. Meo, Differential logic programming, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.359-370, March 1993, Charleston, South Carolina, United States
|
|
|
|
|
|
|
|
|
Tadashi Kanamori , Hiroshi Fujita , Hirohisa Seki , Kenji Horiuchi , Machi Maeji, Argus/V: a system for verification of Prolog programs, Proceedings of 1986 ACM Fall joint computer conference, p.994-999, November 1986, Dallas, Texas, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Marc Denecker , Victor Marek , Miroslaw Truszczyński, Approximations, stable operators, well-founded fixpoints and applications in nonmonotonic reasoning, Logic-based artificial intelligence, Kluwer Academic Publishers, Norwell, MA, 2000
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
C. Beeri , S. Naqvi , R. Ramakrishnan , O. Shmueli , S. Tsur, Sets and negation in a logic data base language (LDL1), Proceedings of the sixth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.21-37, March 23-25, 1987, San Diego, California, United States
|
|
|
Bharat Jayaraman , Frank S. K. Silbermann, Equations, sets, and reduction semantics for functional and logic programming, Proceedings of the 1986 ACM conference on LISP and functional programming, p.320-331, August 1986, Cambridge, Massachusetts, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Marianne Baudinet , Marc Niézette , Pierre Wolper, On the representation of infinite temporal data and queries (extended abstract), Proceedings of the tenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.280-290, May 29-31, 1991, Denver, Colorado, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Michael Codish , Harald Søndergaard, Meta-circular abstract interpretation in prolog, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
D. Chimenti , R. Gamboa , R. Krishnamurthy , S. Naqvi , S. Tsur , C. Zaniolo, The LDL System Prototype, IEEE Transactions on Knowledge and Data Engineering, v.2 n.1, p.76-90, March 1990
|
|
|
Judy Goldsmith , Robert H. Sloan , Balázs Szörényi , György Turán, Theory revision with queries: horn, read-once, and parity formulas, Artificial Intelligence, v.156 n.2, p.139-176, July 2004
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Hai-Feng Guo , Bharat Jayaraman , Gopal Gupta , Miao Liu, Optimization with mode-directed preferences, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.242-251, July 11-13, 2005, Lisbon, Portugal
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
J. Herath , Y. Yamaguchi , N. Saito , T. Yuba, Dataflow Computing Models, Languages, and Machines for Intelligence Computations, IEEE Transactions on Software Engineering, v.14 n.12, p.1805-1828, December 1988
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
W. Vasconcelos , D. Robertson , C. Sierra , M. Esteva , J. Sabater , M. Wooldridge, Rapid Prototyping of Large Multi-Agent Systems Through Logic Programming, Annals of Mathematics and Artificial Intelligence, v.41 n.2-4, p.135-169, August 2004
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Davy Van Nieuwenborgh , Stijn Heymans , Dirk Vermeir, Approximating Extended Answer Sets, Proceeding of the 2006 conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 -- September 1, 2006, Riva del Garda, Italy, p.462-466, May 22, 2006
|
|
|
|
|
|
A. Colmerauer , H. Kanoui , M. Van Caneghem, Last steps towards an ultimate Prolog, Proceedings of the 7th international joint conference on Artificial intelligence, p.947-948, August 24-28, 1981, Vancouver, BC, Canada
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Luis Moniz Pereira , Joaquim N. Aparicio , Jose J. Alferes, Derivation procedures for extended stable models, Proceedings of the 12th international joint conference on Artificial intelligence, p.863-868, August 24-30, 1991, Sydney, New South Wales, Australia
|
|
|
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
I.2