DPLL-based procedure for equality logic with uninterpreted functions

O. Tveretina

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic


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.
Original languageEnglish
Title of host publicationContributions to the Doctoral Programme of the Second International Joint Conference on Automated Reasoning (IJCAR 2004, Cork, Ireland, July 4-8, 2004)
EditorsU. Sattler
Publication statusPublished - 2004

Publication series

NameCEUR Workshop Proceedings
ISSN (Print)1613-0073

Cite this