A Proof System and a Decision Procedure for Equality Logic

Abstract. Equality logic with or without uninterpreted functions is used for proving the equivalence or refinement between systems (hardware verification, compiler’s translation, etc). Current approaches for deciding this type of formulas mainly use a transformation of an equality formula to the propositional formula of larger size, and then any standard SAT checker can be applied. We give an approach for deciding satisfiability of equality logic formu-las in conjunctive normal form (E-CNF) without a transformation to the propositional one. Central in our approach is a single proof rule for which we prove soundness and completeness. Based on this rule the complete procedure for E-SAT have been proposed and its correctness proved. For proving completeness of the proof rule and the algorithm we introduce a general theorem globalizing a local commutation criterion for different proof systems. Techniques for removing clauses preserving the satisfiability behavior are given. Applying our procedure on a variation of the pigeon hole formula yields a polynomial complexity contrary to earlier approaches to E-SAT