max planck institut
informatik

# MPI-I-2009-RG1-001

## 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$.
Acknowledgement:
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
389 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: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2009-RG1-001
BibTeX
@TECHREPORT{HorbachWeidenbach2009,
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},
}