@techreport{HorbachWeidenbach2009,
TITLE = {Deciding the Inductive Validity of Forall Exists* Queries},
AUTHOR = {Horbach, Matthias and Weidenbach, Christoph},
LANGUAGE = {eng},
NUMBER = {MPI-I-2009-RG1-001},
LOCALID = {Local-ID: C125716C0050FB51-F9BA0666A42B8463C12576AF002882D7-Horbach2009TR1},
YEAR = {2009},
DATE = {2009},
ABSTRACT = {We present a new saturation-based decidability result for inductive validity. Let $\Sigma$ 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\{A_1,\ldots,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$.},
}