# 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 ? And the following ? ## Axioms for Term Algebras

Term algebra axioms for function symbols (recall Unification): and for and 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: Additional axiom schema for finite terms: if is a term containing but not identical to .

## Unification as Decision Procedure

Represent each disequation as where are fresh variables.

Unification represents the set of all solutions of positive literals.

If the mgu does not have same values for and , then there is a ground substitution that assigns and different ground terms. More generally,

Theorem: Let be a set of equations and disequations where disequations are only between variables. Let the unification problem for equations in . Then

• if has no unifier, the set is unsatisfiable over ground terms;
• if has a most general unifier such that for all we have , 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 is satisfiable.

Note: we need assumption that there are infinitely many terms, consider for example and formula .

## 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. implies ).

## Selector Symbols

They are useful for avoiding the need for variables.

We represent by const/car/cdr: one binary function symbol, cons

Represent by here

• is negation of • is • is .

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