Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Deciding the inductive validity of $\forall\exists^*$ queries

Horbach, Matthias and Weidenbach, Christoph

MPI-I-2009-RG1-001. May 2009, 43 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
We present a new saturation-based decidability result for
inductive validity.
Let $\Signature$ be a finite signature in which all function symbols are
at most unary and let $N$ be a satisfiable Horn clause set without
equality in which all positive literals are linear.
If $N\cup\{\tenum{A}{n}\rightarrow\}$ belongs to a finitely saturating
clause class, then it is decidable whether a sentence of the form
$\forall\exists^* (A_1\wedge\ldots\wedge A_n)$ is valid in the minimal
model of $N$.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-2009-RG1-001.pdf389 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Horbach, Matthias and Weidenbach, Christoph},
  TITLE = {Deciding the inductive validity of $\forall\exists^*$ queries},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-2009-RG1-001},
  MONTH = {May},
  YEAR = {2009},
  ISSN = {0946-011X},