Given a FOL formula with equality and without quantifiers, we wish to check whether it is satisfiable (does there exist an interpretation that makes this formula true).

We do not restrict ourselves to any particular class of structures, we look at all possible structures.

Based on what we learned so far, how can we solve this problem? Skolemize. Apply paramodulation (see Definition of resolution for FOL and Proof Rule for Equality.)

Example: is the following formula satisfiable: \[

a=f(a) \land a \neq b

\] is 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)

\]

Recall Herbrand Universe for Equality.

What can we assume about the domain of interpretations of ? they are interpreted over elements of factor structure of ground terms

Recall Axioms for Equality.

Suppose that there exists a model. What do we know about the congruence?

The family of all congruences that contain a given relation.

Closure under intersection.

Existence of smallest congruence containing a given relation.

Iterative algorithm for finding congruence closure.

• Decision Procedures Based on Congruence Closure
• Greg Nelson's PhD thesis: Techniques for Program Verification, Stanford, 1981