1 Search Results for "Drabent, Wlodzimierz"

Document
DOI: 10.4230/LIPIcs.ICLP.2012.301
Logic + control: An example

Authors: Wlodzimierz Drabent

Published in: LIPIcs, Volume 17, Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (2012)

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.
Cite as

Wlodzimierz Drabent. Logic + control: An example. In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 17, pp. 301-311, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{drabent:LIPIcs.ICLP.2012.301,
  author =	{Drabent, Wlodzimierz},
  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 =	{Dovier, Agostino and Santos Costa, V{\'\i}tor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2012.301},
  URN =		{urn:nbn:de:0030-drops-36317},
  doi =		{10.4230/LIPIcs.ICLP.2012.301},
  annote =	{Keywords: program correctness, program completeness, specification, declarative programming, declarative diagnosis.}
}
  • Refine by Author
  • 1 Drabent, Wlodzimierz

  • Refine by Classification

  • Refine by Keyword
  • 1 declarative diagnosis.
  • 1 declarative programming
  • 1 program completeness
  • 1 program correctness
  • 1 specification

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2012

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact