Deciding Quantifier-Free First-Order Logic Formulas

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:

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

is the following

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