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.
Example: is the following formula satisfiable:
is the following