Silvio Ghilardi ; Alessandro Gianola ; Deepak Kapur - Uniform Interpolants in EUF: Algorithms using DAG-representations

lmcs:7257 - Logical Methods in Computer Science, April 14, 2022, Volume 18, Issue 2 - https://doi.org/10.46298/lmcs-18(2:2)2022
Uniform Interpolants in EUF: Algorithms using DAG-representationsArticle

Authors: Silvio Ghilardi ; Alessandro Gianola ORCID; Deepak Kapur

    The concept of uniform interpolant for a quantifier-free formula from a given formula with a list of symbols, while well-known in the logic literature, has been unknown to the formal methods and automated reasoning community for a long time. This concept is precisely defined. Two algorithms for computing quantifier-free uniform interpolants in the theory of equality over uninterpreted symbols (EUF) endowed with a list of symbols to be eliminated are proposed. The first algorithm is non-deterministic and generates a uniform interpolant expressed as a disjunction of conjunctions of literals, whereas the second algorithm gives a compact representation of a uniform interpolant as a conjunction of Horn clauses. Both algorithms exploit efficient dedicated DAG representations of terms. Correctness and completeness proofs are supplied, using arguments combining rewrite techniques with model theory.


    Volume: Volume 18, Issue 2
    Published on: April 14, 2022
    Accepted on: February 14, 2022
    Submitted on: March 9, 2021
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • AF: Small: Comprehensive Groebner, Parametric GCD Computations and Real Geometric Reasoning; Funder: National Science Foundation; Code: 1908804

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1585 times.
    This article's PDF has been downloaded 865 times.