Decision Procedures for Equality Logic with Uninterpreted Functions

Abstract. The equality logic with uninterpreted functions (EUF) has been proposed for processor verification. A procedure for proving satis-fiability of formulas in this logic is introduced. Since it is based on the DPLL method, the procedure can adopt its heuristics. Therefore the pro-cedure can be used as a basis for efficient implementations of satisfiability checkers for EUF. A part of the introduced method is a technique for reducing the size of formulas, which can also be used as a preprocessing step in other approaches for checking satisfiability of EUF formulas