LARA

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 ?

\begin{equation*} a=f(a) \land a \neq b \end{equation*}

And the following ?

\begin{equation*} (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) \end{equation*}

Axioms for Term Algebras

Term algebra axioms for function symbols (recall Unification):

\begin{equation*} \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 \end{equation*}

and

\begin{equation*} \forall x_1,\ldots,x_n,y_1,\ldots,y_m.\ f(x_1,\ldots,x_n) \neq g(y_1,\ldots,y_m) \end{equation*}

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:

\begin{equation*} \forall x. \bigvee_{f \in {\cal L}} \exists y_1,\ldots,y_{ar(f)}.\ x=f(y_1,\ldots,y_{ar(f)}) \end{equation*}

Additional axiom schema for finite terms:

\begin{equation*} \forall x. t(x) \neq x \end{equation*}

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

\begin{equation*} x_1 = t_1 \land x_2 = t_2 \land x_1 \neq x_2 \end{equation*}

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

\begin{equation*} x=car(x) \land y = cdr(z) \land \lnot atom(z) \end{equation*}

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