DPLL-based procedure for equality logic with uninterpreted functions

O. Tveretina

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review


    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


    Dive into the research topics of 'DPLL-based procedure for equality logic with uninterpreted functions'. Together they form a unique fingerprint.

    Cite this