When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.05171.5
URN: urn:nbn:de:0030-drops-2598
Go to the corresponding Portal

Marek, Victor W. ; Remmel, Jeffrey B.

Normal Form Theorem for Logic Programs with Cardinality Constraints

05171.MarekVictor.Paper.259.pdf (0.4 MB)


We discuss proof schemes, a kind of context-dependent proofs for logic
programs. We show usefullness of these constructs both in the context of
normal logic programs and their generalizations due to Niemela and
collaborators. As an application we show the following result. For every
cardinality-constraint logic program P there is a logic program P´ with the
same heads, but with bodies consisting of atoms and negated atoms such
that P and P´ have same stable models. It is worth noting that another
proof of same result can be obtained from the results by Lifschitz and

BibTeX - Entry

  author =	{Marek, Victor W. and Remmel, Jeffrey B.},
  title =	{{Normal Form Theorem for Logic Programs with Cardinality Constraints}},
  booktitle =	{Nonmonotonic Reasoning, Answer Set Programming and Constraints},
  pages =	{1--34},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5171},
  editor =	{Gerhard Brewka and Ilkka Niemel\"{a} and Torsten Schaub and Miroslaw Truszczynski},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-2598},
  doi =		{10.4230/DagSemProc.05171.5},
  annote =	{Keywords: Proof scheme, cardinality constraints}

Keywords: Proof scheme, cardinality constraints
Collection: 05171 - Nonmonotonic Reasoning, Answer Set Programming and Constraints
Issue Date: 2005
Date of publication: 14.09.2005

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