EufDPLL -- A tool to check satisfiability of equality logic formulas. 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.
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Tveretina, Olga; Wesselink, Wieger: EufDPLL -- a tool to check satisfiability of equality logic formulas (2008)