A decision procedure for equality logic with uninterpreted functions

O. Tveretina

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

    2 Citations (Scopus)

    Abstract

    The equality logic with uninterpreted functions (EUF) has been proposed for processor verification. A procedure for proving satisfiability of formulas in this logic is introduced. Since it is based on the DPLL method, the procedure can adopt its heuristics. Therefore the procedure can be used as a basis for efficient implementations of satisfiability checkers for EUF. A part of the introduced method is a technique for reducing the size of formulas, which can also be used as a preprocessing step in other approaches for checking satisfiability of EUF formulas.
    Original languageEnglish
    Title of host publicationArtificial Intelligence and Symbolic Computation (Proceedings 7th International Conference, AISC 2004, Linz, Austria, September 22-24, 2004)
    EditorsB. Buchberger, J.A. Campbell
    Place of PublicationBerlin
    PublisherSpringer
    Pages66-79
    ISBN (Print)3-540-23212-5
    DOIs
    Publication statusPublished - 2004

    Publication series

    NameLecture Notes in Computer Science
    Volume3249
    ISSN (Print)0302-9743

    Cite this