# Item

ITEM ACTIONSEXPORT

Released

Report

#### Deciding the Inductive Validity of Forall Exists* Queries

##### External Resource

No external resources are shared

##### Fulltext (restricted access)

There are currently no full texts shared for your IP range.

##### Fulltext (public)

decIndQueries_TR.pdf

(Any fulltext), 391KB

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Horbach, M., & Weidenbach, C.(2009). *Deciding the Inductive
Validity of Forall Exists* Queries* (MPI-I-2009-RG1-001).

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-1A51-3

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