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 |