MPI-INF/SWS Research Reports 1991-2021

2. Number - only RG1


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

Horbach, Matthias and Weidenbach, Christoph

May 2009, 43 pages.

Status: available - back from printing

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$.

  • MPI-I-2009-RG1-001.pdf
  • Attachement: MPI-I-2009-RG1-001.pdf (389 KBytes)

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},