License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICLP.2011.280
URN: urn:nbn:de:0030-drops-31875
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3187/
Go to the corresponding LIPIcs Volume Portal

Kriener, Jael

Correct Reasoning about Logic Programs

pdf-format:
30.pdf (0.2 MB)

Abstract

In this PhD project, we present an approach to the problem of determinacy inference in logic programs with cut, which treats cut uniformly and contextually. The overall aim is to develop a theoretical analysis, abstract it to a suitable domain and prove both the concrete analysis and the abstraction correct in a formal theorem prover (Coq). A crucial advantage of this approach, besides the guarantee of correctness, is the possibility of automatically extracting an implementation of the analysis.

BibTeX - Entry

@InProceedings{kriener:LIPIcs:2011:3187,
  author =	{Jael Kriener},
  title =	{{Correct Reasoning about Logic Programs }},
  booktitle =	{Technical Communications of the 27th International Conference on Logic Programming (ICLP'11) },
  pages =	{280--283},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-31-6},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{11},
  editor =	{John P. Gallagher and Michael Gelfond},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3187},
  URN =		{urn:nbn:de:0030-drops-31875},
  doi =		{10.4230/LIPIcs.ICLP.2011.280},
  annote =	{Keywords: Prolog, cut, determinacy inference, abstract interpretation, denotational semantics, automated theorem proving, Coq}
}

Keywords: Prolog, cut, determinacy inference, abstract interpretation, denotational semantics, automated theorem proving, Coq
Collection: Technical Communications of the 27th International Conference on Logic Programming (ICLP'11)
Issue Date: 2011
Date of publication: 27.06.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI