Theorem-proving with resolution and superposition

AbstractWe present a refutationally complete set of inference rules for first-order logic with equality. Except for x = x, no equality axioms are needed. Equalities are oriented by a well-founded ordering and can be used safely for demodulation without losing completeness. When restricted to equational logic, this strategy reduces to a Knuth-Bendix procedure