liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
Logic + Control: An Example
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology. Institute of Computer Science, Polish Academy of Sciences. (TCSLAB)
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)
Abstract [en]

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
Keyword [en]
Logic programming, program correctness, program completeness, specication, declarative programming, declarative diagnosis
National Category
Computer Science
URN: urn:nbn:se:liu:diva-79508DOI: 10.4230/LIPIcs.ICLP.2012.301ISBN: 978-3-939897-43-9OAI: diva2:543156
28th International Conference on Logic Programming (ICLP-2012), 4-8 September, Budapest, Hungary
Available from: 2012-08-06 Created: 2012-08-06 Last updated: 2014-11-04Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Drabent, Wlodzimierz
By organisation
Software and SystemsThe Institute of Technology
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 49 hits
ReferencesLink to record
Permanent link

Direct link