Differences
This shows you the differences between two versions of the page.
|
sav08:deciding_quantifier-free_fol_over_ground_terms [2008/05/19 14:04] vkuncak |
sav08:deciding_quantifier-free_fol_over_ground_terms [2015/04/21 17:30] |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Deciding Quantifier-Free FOL over Ground Terms ====== | ||
| - | |||
| - | Instead of considering arbitrary interpretations, consider now satisfiability over an interpretation of ground terms. | ||
| - | |||
| - | For now also no relation symbols. | ||
| - | |||
| - | What is the difference compared to models considered in [[Deciding Quantifier-Free FOL]]? | ||
| - | |||
| - | Can we treat variables as constants in this case? | ||
| - | |||
| - | Is the following formula satisfiable ? | ||
| - | \[ | ||
| - | a=f(a) \land a \neq b | ||
| - | \] ++|No. When interpreting variables as constants, two syntactically different terms are different ($a \neq f(a)$).++ | ||
| - | |||
| - | |||
| - | And the following ? | ||
| - | \[ | ||
| - | (f(a)=b \lor (f(f(f(a))) = a \land f(a) \neq f(b))) \land f(f(f(f(a)) \neq b \land b=f(b) | ||
| - | \] | ||
| - | |||
| - | ===== Axioms for Term Algebras ===== | ||
| - | |||
| - | Term algebra axioms for function symbols (recall [[Unification]]): | ||
| - | \[ | ||
| - | \forall x_1,\ldots,x_n,y_1,\ldots,y_n.\ f(x_1,\ldots,x_n)=f(y_1,\ldots,y_n) \rightarrow \bigwedge_{i=1}^n x_i=y_i | ||
| - | \] | ||
| - | and | ||
| - | \[ | ||
| - | \forall x_1,\ldots,x_n,y_1,\ldots,y_m.\ f(x_1,\ldots,x_n) \neq g(y_1,\ldots,y_m) | ||
| - | \] | ||
| - | for $g$ and $f$ distinct symbols. | ||
| - | |||
| - | Unless the language is infinite, we have that each element is either a constant or is result of application of some function symbols: | ||
| - | \[ | ||
| - | \forall x. \bigvee_{f \in {\cal L}} \exists y_1,\ldots,y_{ar(f)}.\ x=f(y_1,\ldots,y_{ar(f)}) | ||
| - | \] | ||
| - | |||
| - | Additional axiom schema for finite terms: | ||
| - | \[ | ||
| - | \forall x. t(x) \neq x | ||
| - | \] | ||
| - | if $t(x)$ is a term containing $x$ but not identical to $x$. | ||
| - | |||
| - | ===== Unification as Decision Procedure ===== | ||
| - | |||
| - | Represent each disequation $t_1 \neq t_2$ as | ||
| - | \[ | ||
| - | x_1 = t_1 \land x_2 = t_2 \land x_1 \neq x_2 | ||
| - | \] | ||
| - | where $x_1,x_2$ are fresh variables. | ||
| - | |||
| - | Unification represents the set of all solutions of positive literals. | ||
| - | |||
| - | If the mgu does not have same values for $x_1$ and $x_2$, then there is a ground substitution that assigns $x_1$ and $x_2$ different ground terms. More generally, | ||
| - | |||
| - | **Theorem:** Let $E$ be a set of equations and disequations where disequations are only between variables. Let $E^+ = \{ (t_1 \doteq t_2) \mid (t_1 = t_2) \in E \}$ the unification problem for equations in $E$. Then | ||
| - | * if $E^+$ has no unifier, the set $E$ is unsatisfiable over ground terms; | ||
| - | * if $E^+$ has a most general unifier $\sigma$ such that for all $(x \neq y) \in E$ we have $\sigma(x) \neq \sigma(y)$, then if the language contains at least one function symbol of arity at least one (i.e. the set of ground terms is infinite) then $E$ is satisfiable. | ||
| - | |||
| - | Note: we need assumption that there are infinitely many terms, consider for example ${\cal L} = \{ a,b\}$ and formula $x \neq y \land x \neq z \land y \neq z$. | ||
| - | |||
| - | ===== Algorithmic Aspects ===== | ||
| - | |||
| - | We can use DAGs and union-find as well. | ||
| - | |||
| - | The result is similar to checking satisfiability of ground formulas over arbitrary interpretations (but e.g. $f(x)=f(y)$ implies $x=y$). | ||
| - | |||
| - | ===== Selector Symbols ===== | ||
| - | |||
| - | They are useful for avoiding the need for variables. | ||
| - | |||
| - | We represent $f(x,y)=z$ by $Is_f(z) \land x = f_1(z) \land y = f_2(z)$ | ||
| - | |||
| - | const/car/cdr: one binary function symbol, cons | ||
| - | |||
| - | Represent $cons(x,y)=z$ by | ||
| - | \[ | ||
| - | x=car(x) \land y = cdr(z) \land \lnot atom(z) | ||
| - | \] | ||
| - | here | ||
| - | * $atom(x)$ is negation of $Is_{cons}$ | ||
| - | * $car$ is $cons_1$ | ||
| - | * $cdr$ is $cons_2$. | ||
| - | |||
| - | ===== Notes on Decidability ===== | ||
| - | |||
| - | For quantifier-free formulas, satisfiability is decidable, whether or not we have predicate symbols as well. | ||
| - | |||
| - | Let us clarify the status of quantified constraints. | ||
| - | |||
| - | In Herbrand interpretation we interpret functions and constants as themselves (their interpretation is fixed) but we interpret predicates as arbitrary predicates on ground terms. | ||
| - | |||
| - | So, for quantified case: | ||
| - | * if we have no predicates: theory is decidable, using quantifier elimination (these structures are called "term algebras", see [[List of Theories Admitting QE]]) | ||
| - | * if we have predicates: this is satisfiability in Herbrand models, equivalent to satisfiability in FOL without equality, so it is undecidable | ||
| - | |||
| - | ===== References ===== | ||
| - | |||
| - | * [[http://lara.epfl.ch/~kuncak/papers/KuncakRinard03TheoryStructuralSubtyping.html|On the Theory of Structural Subtyping]], see Lemma 25 on page 13 | ||