Cited By
View all- Cristiá MRossi G(2019)Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary RelationsJournal of Automated Reasoning10.1007/s10817-019-09520-464:2(295-330)Online publication date: 8-Apr-2019
Constraint logic programming with a relational machine
Pages 97 - 124
Abstract
We present a declarative framework for the compilation of constraint logic programs into variable-free relational theories which are then executed by rewriting. This translation provides an algebraic formulation of the abstract syntax of logic programs. Logic variables, unification, and renaming apart are completely elided in favor of manipulation of variable-free relation expressions. In this setting, term rewriting not only provides an operational semantics for logic programs, but also a simple framework for reasoning about program execution. We prove the translation sound, and the rewriting system complete with respect to traditional SLD semantics.
References
References
[1]
Amato G, Lipton J, McGrail R (2009) On the algebraic structure of declarative programming languages. Theor Comput Sci 410(46):4626–4671. (Abstract of professor Giorgio Levi)
[2]
Asperti A, Martini S (1989) Projections instead of variables: a category theoretic interpretation of logic programs. In: ICLP, pp 337–352
[3]
Broome P, Lipton J (1994) Combinatory logic programming: computing in relation calculi. In: Proceedings of the 1994 international symposium on logic programming (ILPS’94). MIT Press, Cambridge, pp 269–285
[4]
Bellia M and Occhiuto ME C-expressions: a variable-free calculus for equational logic programming Theor Comput Sci 1993 107 2 209-252
[5]
Clark KL (1977) Negation as failure. In: Gallaire H, Minker J (eds) Logic and data bases. Plenum Press, New York, pp 293–322
[6]
Cheney J, Urban C (2004) Alpha-Prolog: A logic programming language with names, binding and alpha-equivalence. In: Demoen B,Lifschitz V(eds) Proceedings of the 20th Conference on Logic Programming ICLP2004. Lecture Notes in Computer Science, vol 3132. Springer, New York, pp 269–283
[7]
Finkelstein SE, Freyd PJ, and Lipton J A new framework for declarative programming Theor Comput Sci 2003 300 1–3 91-160
[8]
Freyd PJ and Scedrov A Categories, allegories 1991 Amsterdam North Holland Publishing Company
[9]
Gallego Arias E, Lipton J (2012) Logic programming in tabular allegories. In: Dovier A, Santos Costa (eds) Technical communications of the 28th international conference on logic programming (ICLP’12), Budapest. LIPIcs, vol 17, pp 334–347. Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik
[10]
Gallego Arias E, Lipton J, Mariño J, and Nogueira P First-order unification using variable-free relational algebra Log J IGPL 2011 19 6 790-820
[11]
Gallego Arias E, Lipton J, Mariño J (2015) Declarative compilation for constraint logic programming. In: Proietti M, Seki H (eds) Logic-based program synthesis and transformation. Lecture notes in computer science, vol 8981. Springer, New York, pp 299–316
[12]
Hamfelt A, Fischer Nilsson J (1998) Inductive synthesis of logic programs by composition of combinatory program schemes. In: Flener P (ed) 8th international workshop on logic-based program synthesis and transformation (LOPSTR’98). Lecture notes in computer science, vol 1559. Springer, New York, pp 143–158
[13]
Hamfelt A, Nilsson JF, Vitoria A (1998) A combinatory form of pure logic programs and its compositional semantics. Technical report
[14]
Jaffar J, Maher MJ (1994) Constraint logic programming: a survey. J Log Program, 19/20:503–581
[15]
Kinoshita Y, John Power A (1996) A fibrational semantics for logic programs. In: Dyckhoff R, Herre H, Schroeder-Heister P (eds) ELP. Lecture notes in computer science, vol 1050. Springer, New York, pp 177–191
[16]
Komendantskaya E, Power J (2011) Coalgebraic derivations in logic programming. In: Bezem M (ed) CSL. LIPIcs, vol 12, pp 352–366. Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik
[17]
Lipton J, Chapman E (1998) Some notes on logic programming with a relational machine. In: Jaoua A, Kempf P, Schmidt G (eds) Using relational methods in computer science. Technical report Nr. 1998-03, pp 1–34. Fakultät fär Informatik, Universität der Bundeswehr Mänchen
[18]
Lloyd JW Foundations of logic programming 1984 New York Springer
[19]
Miller D, Nadathur G, Pfenning F, and Scedrov A Uniform proofs as a foundation for logic programming Ann Pure Appl Log 1991 51 1–2 125-157
[20]
Nilsson JF (1990) Combinatory logic programming. In: Procs. of the 2nd workshop on meta-programming in logic. K.U. Leuven, Belgium
[21]
Pfenning F, Elliot C (1988) Higher-order abstract syntax. In: Proceedings of the ACM SIGPLAN 1988 conference on programming language design and implementation (PLDI’88). ACM, New York, pp 199–208
[22]
Rydeheard DE, Burstall RM (1986) A categorical unification algorithm. In: Proceedings of a tutorial and workshop on category theory and computer programming. Springer, New York, pp 493–505
[23]
Tarski A, Givant S (1987) A formalization of set theory without variables. In: Colloquium publications, vol 41. American Mathematical Society, Providence
[24]
Urban C, Pitts AM, and Gabbay MJ Nominal unification Theor Comput Sci 2004 323 1–3 473-497
Index Terms
- Constraint logic programming with a relational machine
Index terms have been assigned to the content through auto-classification.
Recommendations
From answer set logic programming to circumscription via logic of GK
We first embed Pearce's equilibrium logic and Ferraris's propositional general logic programs in Lin and Shoham's logic of GK, a nonmonotonic modal logic that has been shown to include as special cases both Reiter's default logic in the propositional ...
Nominal logic programming
Nominal logic is an extension of first-order logic which provides a simple foundation for formalizing and reasoning about abstract syntax modulo consistent renaming of bound names (that is, α-equivalence). This article investigates logic programming ...
‘Classical’ Negation in Nonmonotonic Reasoning and Logic Programming
Gelfond and Lifschitz were the first to point out the need for a symmetric negation in logic programming and they also proposed a specific semantics for such negation for logic programs with the stable semantics, which they called ‘classical’. Subsequently,...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© British Computer Society 2016.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 January 2017
Accepted: 10 March 2016
Revision received: 11 January 2016
Received: 02 July 2015
Published in FAC Volume 29, Issue 1
Author Tags
Qualifiers
- Research-article
Funding Sources
- Wesleyan University Research Grant
- Comunidad de Madrid
- MINECO
- ANR
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 77Total Downloads
- Downloads (Last 12 months)57
- Downloads (Last 6 weeks)28
Reflects downloads up to 12 Dec 2024
Other Metrics
Citations
Cited By
View all- Cristiá MRossi G(2019)Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary RelationsJournal of Automated Reasoning10.1007/s10817-019-09520-464:2(295-330)Online publication date: 8-Apr-2019
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in