TY - GEN
T1 - DPLL-based procedure for equality logic with uninterpreted functions
AU - Tveretina, O.
PY - 2004
Y1 - 2004
N2 - The logic of equality with uninterpreted functions (EUF) has been proposed for processor verification. We describe EDPLL, a calculus for proving satisfiability of formulas in this kind of logic. Being based
on the DPLL procedure, EDPLL can adopt heuristics developed for this method.
AB - The logic of equality with uninterpreted functions (EUF) has been proposed for processor verification. We describe EDPLL, a calculus for proving satisfiability of formulas in this kind of logic. Being based
on the DPLL procedure, EDPLL can adopt heuristics developed for this method.
M3 - Conference contribution
T3 - CEUR Workshop Proceedings
BT - Contributions to the Doctoral Programme of the Second International Joint Conference on Automated Reasoning (IJCAR 2004, Cork, Ireland, July 4-8, 2004)
A2 - Sattler, U.
ER -