Decision procedures for subsets of First-Order Logic form the core of many verification tools. Applications include hardware and software verification. The logic of Equality with Uninterpreted Functions (EUF) is a decidable subset of First-Order Logic. The EUF logic and its extensions have been applied for proving equivalence between systems. We present a branch and bound decision procedure for EUF logic based on the generalisation of the Davis-Putnam-Loveland-Logemann procedure (EUF-DPLL). EufDpll is a tool to check satisfiability of EUF formulas based on this procedure.
EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas
Olga Tveretina, Wieger Wesselink
Proceedings of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology
Electronic Notes in Theoretical Computer Science 225:405-420