Cited By
View all- Drabent W(2019)The Prolog Debugger and Declarative ProgrammingLogic-Based Program Synthesis and Transformation10.1007/978-3-030-45260-5_12(193-208)Online publication date: 8-Oct-2019
Proving completeness of logic programs with the cut
Pages 155 - 172
Abstract
Completeness of a logic program means that the program produces all the answers required by its specification. The cut is an important construct of programming language Prolog. It prunes part of the search space, this may result in a loss of completeness. This paper proposes a way of proving completeness of programs with the cut. The semantics of the cut is formalized by describing how SLD-trees are pruned. A sufficient condition for completeness is presented, proved sound, and illustrated by examples.
References
References
[1]
Andrews JH The witness properties and the semantics of the Prolog cut TPLP 2003 3 1 1-59
[2]
Apt KR and Pedreschi D Reasoning about termination of pure Prolog programs Inf Comput 1993 106 1 109-157
[3]
Apt KR (1997) From logic programming to Prolog. International Series in Computer Science. Prentice Hall Europe, Hemel Hempstead, Hertfordshire
[4]
Bossi A and Cocco N Díaz J and Orejas F Verifying correctness of logic programs TAPSOFT, Vol.2, Lecture Notes in Computer Science, vol 352. 1989 Berlin Heidelberg Springer 96-110
[5]
Bezem M Strong termination of logic programs J Log Program 1993 15 1&2 79-97
[6]
Billaud M Simple operational and denotational semantics for Prolog with cut Theor Comput Sci 1990 71 2 193-208
[7]
Clark KL (1979) Predicate logic as computational formalism. Technical Report 79/59, Imperial College, London
[8]
Deransart P Proof methods of declarative properties of definite programs Theor Comput Sci 1993 118 2 99-166
[9]
Drabent W and Małuszyński J Inductive assertion method for logic programs Theor Comput Sci 1988 59 133-155
[10]
Deransart P and Małuszyński J A Grammatical view of logic programming 1993 Cambridge, Massachusetts, London, England The MIT Press
[11]
Drabent W and Miłkowska M Proving correctness and completeness of normal programs – a declarative approach TPLP 2005 5 6 669-711
[12]
Doets K From logic to logic programming 1994 Cambridge The MIT Press
[13]
Drabent W (2015) On completeness of logic programs. In: Logic based program synthesis and transformation, LOPSTR 2014. Revised Selected Papers, Lecture Notes in Computer Science, vol 8981. Springer, Berlin. Extended version in CoRR (2014). arXiv:1411.3015.
[14]
Drabent W Correctness and completeness of logic programs ACM Trans Comput Log 2016 17 3 18-11832
[15]
Drabent W On definite program answers and least Herbrand models TPLP 2016 16 4 498-508
[16]
de Vink EP Comparative semantics for PROLOG with cut Sci Comput Program 1989 13 1 237-264
[17]
Kriener J, King A (2014) Semantics for Prolog with cut-revisited. In: Codish M, Sumii E (eds) Functional and Logic Programming—12th International Symposium, FLOPS 2014, Kanazawa, Japan, June 4–6, 2014. Proceedings, Lecture Notes in Computer Science, vol 8475. Springer, Berlin, pp 270–284
[18]
Lloyd JW, (1987) Foundations of logic programming. Second, extended edition. Springer, Berlin
[19]
Maher MJ (1988) Equivalences of logic programs. In: Minker J (ed) Foundations of deductive databases and logic programming. Morgan Kaufmann, Los Altos, California, pp 627–658
[20]
Nilsson U, Małuszyński J (1995) Logic, programming and Prolog (2ed). Wiley, Chichester, West Sussex, England. http://www.ida.liu.se/~ulfni/lpp/.
[21]
Schneider-Kamp P, Giesl J, Ströder T, Serebrenik A, and Thiemann R Automated termination analysis for logic programs with cut TPLP 2010 10 4-6 365-381
[22]
Shapiro E Algorithmic program debugging 1983 Cambridge, Massachusetts, London, England The MIT Press
[23]
Spoto F Operational and goal-independent denotational semantics for Prolog with cut J Log Program 2000 42 1 1-46
[24]
Sterling L and Shapiro E The art of Prolog 1994 2 Cambridge, Massachusetts, London, England The MIT Press
Index Terms
- Proving completeness of logic programs with the cut
Index terms have been assigned to the content through auto-classification.
Recommendations
Correctness and Completeness of Logic Programs
We discuss proving correctness and completeness of definite clause logic programs. We propose a method for proving completeness, while for proving correctness we employ a method that should be well known but is often neglected. Also, we show how to ...
Completeness and Cut-elimination in the Intuitionistic Theory of Types
In this paper we define a model theory and give a semantic proof of cut-elimination for ICTT, an intuitionistic formulation of Church's theory of types defined by Miller et al. and the basis for the λProlog programming language. Our approach, extending ...
On Correctness of Normal Logic Programs
Logic-Based Program Synthesis and TransformationAbstractWe present sufficient conditions for correctness of logic programs with negation (normal programs). We focus on the Kunen semantics, this declarative semantics is a closest one to what is implemented in Prolog (negation by finite failure) when ...
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: 20 July 2016
Received: 03 July 2015
Published in FAC Volume 29, Issue 1
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 38Total Downloads
- Downloads (Last 12 months)18
- Downloads (Last 6 weeks)2
Reflects downloads up to 11 Dec 2024
Other Metrics
Citations
Cited By
View all- Drabent W(2019)The Prolog Debugger and Declarative ProgrammingLogic-Based Program Synthesis and Transformation10.1007/978-3-030-45260-5_12(193-208)Online publication date: 8-Oct-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