Proving completeness of logic programs with the cut

DOI10.1007/S00165-016-0392-0MaRDI QIDQ511027zbMATH OpenOpenAlexWikidataFDO

Authors Włodzimierz Drabent

Publication date 14 February 2017

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1602.08778

zbMATH Keywords

cutlogic programmingoperational semanticsprogram completenessprogram correctness

Mathematics Subject Classification ID

Logic programming (68N17)

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.

Recommendations

• On completeness of logic programs
• scientific article; zbMATH DE number 515746
• Correctness and completeness of logic programs
• scientific article; zbMATH DE number 4045228
• Proving properties of committed choice logic programs

Cites work

• Automated termination analysis for logic programs with cut
• Comparative semantics for prolog with cut
• Correctness and completeness of logic programs
• scientific article; zbMATH DE number 3947593 (Why is no real title available?)
• scientific article; zbMATH DE number 49478 (Why is no real title available?)
• scientific article; zbMATH DE number 708499 (Why is no real title available?)
• scientific article; zbMATH DE number 788036 (Why is no real title available?)
• scientific article; zbMATH DE number 870438 (Why is no real title available?)
• Inductive assertion method for logic pograms
• On completeness of logic programs
• On definite program answers and least Herbrand models
• Operational and goal-independent denotational semantics for Prolog with cut
• Proof methods of declarative properties of definite programs
• Proving correctness and completeness of normal programs – a declarative approach
• Reasoning about termination of pure Prolog programs
• Semantics for Prolog with cut -- revisited
• Simple operational and denotational semantics for Prolog with cut
• Strong termination of logic programs
• The witness properties and the semantics of the Prolog cut

Cited in

(7)

• On completeness of logic programs
• Proving properties of committed choice logic programs
• scientific article; zbMATH DE number 515746 (Why is no real title available?)
• scientific article; zbMATH DE number 1149404 (Why is no real title available?)
• Logic + control: on program construction and verification
• The Prolog debugger and declarative programming
• Completeness for cut-based abduction

This page was built for publication: Proving completeness of logic programs with the cut

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q511027)