Uniform Interpolants in EUF: Algorithms using DAG-representations
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 comp...
Main Authors: | , , |
---|---|
Format: | Article |
Language: | English |
Published: |
Logical Methods in Computer Science e.V.
2022-04-01
|
Series: | Logical Methods in Computer Science |
Subjects: | |
Online Access: | https://lmcs.episciences.org/7257/pdf |
_version_ | 1797268494860943360 |
---|---|
author | Silvio Ghilardi Alessandro Gianola Deepak Kapur |
author_facet | Silvio Ghilardi Alessandro Gianola Deepak Kapur |
author_sort | Silvio Ghilardi |
collection | DOAJ |
description | 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. |
first_indexed | 2024-04-25T01:33:23Z |
format | Article |
id | doaj.art-66443400472b42b987eb82e4ade247d0 |
institution | Directory Open Access Journal |
issn | 1860-5974 |
language | English |
last_indexed | 2024-04-25T01:33:23Z |
publishDate | 2022-04-01 |
publisher | Logical Methods in Computer Science e.V. |
record_format | Article |
series | Logical Methods in Computer Science |
spelling | doaj.art-66443400472b42b987eb82e4ade247d02024-03-08T10:38:41ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742022-04-01Volume 18, Issue 210.46298/lmcs-18(2:2)20227257Uniform Interpolants in EUF: Algorithms using DAG-representationsSilvio GhilardiAlessandro Gianolahttps://orcid.org/0000-0003-4216-5199Deepak KapurThe 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.https://lmcs.episciences.org/7257/pdfcomputer science - logic in computer science |
spellingShingle | Silvio Ghilardi Alessandro Gianola Deepak Kapur Uniform Interpolants in EUF: Algorithms using DAG-representations Logical Methods in Computer Science computer science - logic in computer science |
title | Uniform Interpolants in EUF: Algorithms using DAG-representations |
title_full | Uniform Interpolants in EUF: Algorithms using DAG-representations |
title_fullStr | Uniform Interpolants in EUF: Algorithms using DAG-representations |
title_full_unstemmed | Uniform Interpolants in EUF: Algorithms using DAG-representations |
title_short | Uniform Interpolants in EUF: Algorithms using DAG-representations |
title_sort | uniform interpolants in euf algorithms using dag representations |
topic | computer science - logic in computer science |
url | https://lmcs.episciences.org/7257/pdf |
work_keys_str_mv | AT silvioghilardi uniforminterpolantsineufalgorithmsusingdagrepresentations AT alessandrogianola uniforminterpolantsineufalgorithmsusingdagrepresentations AT deepakkapur uniforminterpolantsineufalgorithmsusingdagrepresentations |