Data di Pubblicazione:
2022
Citazione:
UNIFORM INTERPOLANTS IN EUF: ALGORITHMS USING DAG-REPRESENTATIONS / S. Ghilardi, A. Gianola, D. Kapur. - In: LOGICAL METHODS IN COMPUTER SCIENCE. - ISSN 1860-5974. - 18:2(2022), pp. 1-24. [10.46298/LMCS-18(2:2)2022]
Abstract:
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.
Tipologia IRIS:
01 - Articolo su periodico
Keywords:
DAG representation; EUF; term rewriting; Uniform Interpolation
Elenco autori:
S. Ghilardi, A. Gianola, D. Kapur
Link alla scheda completa:
Link al Full Text: