Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Drabent, Wlodzimierz http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-36317
URL:

Logic + control: An example

pdf-format:


Abstract

We present a Prolog program - the SAT solver of Howe and King - as a (pure) 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 specification. Correctness and termination of the logic program 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 justification is presented. For proving correctness we use a method, which should be well known but is often neglected. For proving program completeness we employ a new, simpler variant of a method published previously. We point out usefulness of approximate specifications. 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.

BibTeX - Entry

@InProceedings{drabent:LIPIcs:2012:3631,
  author =	{Wlodzimierz Drabent},
  title =	{{Logic + control: An example}},
  booktitle =	{Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)},
  pages =	{301--311},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-43-9},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{17},
  editor =	{Agostino Dovier and V{\'i}tor Santos Costa},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3631},
  URN =		{urn:nbn:de:0030-drops-36317},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.ICLP.2012.301},
  annote =	{Keywords: program correctness, program completeness, specification, declarative programming, declarative diagnosis.}
}

Keywords: program correctness, program completeness, specification, declarative programming, declarative diagnosis.
Seminar: Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)
Issue date: 2012
Date of publication: 2012


DROPS-Home | Fulltext Search | Imprint Published by LZI