A proof system and a decision procedure for equality logic

Abstract. We give an approach for deciding satisfiability of equality logic formulas (E-SAT) in conjunctive normal form. Central in our approach is a single proof rule called equality resolution (ER). For this single rule we prove soundness and completeness. Based on this rule we propose a complete procedure for E-SAT and prove its correctness. Applying our procedure on a variation of the pigeon hole formula yields a polynomial complexity contrary to earlier approaches to E-SAT. Parts of the theory we developed for proving completeness of the proof rule and the algorithm are of interest in itself: we give techniques for removing clauses preserving unsatisfiability, and we give a general theorem globalizing a local commutation criterion for different proof systems. Keywords: equality logic, satisfiability, resolution.