Logic + Control: An Example
2012 (English)In: Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) / [ed] Agostino Dovier and Vítor Santos Costa, Dagstuhl Publishing , 2012, 301-311 p.Conference paper, Presentation (Other academic)
We present a Prolog program (the SAT solver of Howe and King) as a logic program with added control. The control consists of a selection rule (delays of Prolog) and pruning the search space. We construct the logic program together with proofs of its correctness and completeness, with respect to a formal specication. This is augmented by a proof of termination under any selection rule. Correctness and termination are inherited by the Prolog program, the change of selection rule preserves completeness. We prove that completeness is also preserved by one case of pruning; for the other an informal justication is presented.
For proving correctness we use a method, which should be well known but is often neglected. A contribution of this paper is a method for proving completeness. In particular we introduce a notion of semi-completeness, for which a local sucient condition exists.
We compare the proof methods with declarative diagnosis (algorithmic debugging). We introduce a method of proving that a certain kind of pruning preserves completeness. We argue that the proof methods correspond to natural declarative thinking about programs, and that they can be used, formally or informally, in every-day programming.
Place, publisher, year, edition, pages
Dagstuhl Publishing , 2012. 301-311 p.
, LIPICS, Leibnitz International Proceedings in Informatics, ISSN 1868-8969 ; Vol. 17
Logic programming, program correctness, program completeness, specication, declarative programming, declarative diagnosis
IdentifiersURN: urn:nbn:se:liu:diva-79508DOI: 10.4230/LIPIcs.ICLP.2012.301ISBN: 978-3-939897-43-9OAI: oai:DiVA.org:liu-79508DiVA: diva2:543156
28th International Conference on Logic Programming (ICLP-2012), 4-8 September, Budapest, Hungary