Refutation calculi for lattice-based logics: from display to tableaux
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911713641627648 |
|---|---|
| author | De Domenico, Andrea Greco, Giuseppe Palmigiano, Alessandra Piazza, Mario Sabatini, Andrea |
| author_facet | De Domenico, Andrea Greco, Giuseppe Palmigiano, Alessandra Piazza, Mario Sabatini, Andrea |
| contents | Refutation calculi are formal systems developed to derive the invalid formulas of a given logic. While the notion of refutation calculi has played a key role in the development of tableaux calculi, a refutation approach to display calculi has not yet been attempted. In this paper, we introduce refutation display calculi for basic LE-logics, i.e., those logics canonically associated with basic normal lattice expansions of any signature. In particular, we prove soundness and completeness via proof-analysis results on derivable sequents. Finally, we obtain terminating tableaux calculi from these refutation display calculi. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_24717 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Refutation calculi for lattice-based logics: from display to tableaux De Domenico, Andrea Greco, Giuseppe Palmigiano, Alessandra Piazza, Mario Sabatini, Andrea Logic Logic in Computer Science Refutation calculi are formal systems developed to derive the invalid formulas of a given logic. While the notion of refutation calculi has played a key role in the development of tableaux calculi, a refutation approach to display calculi has not yet been attempted. In this paper, we introduce refutation display calculi for basic LE-logics, i.e., those logics canonically associated with basic normal lattice expansions of any signature. In particular, we prove soundness and completeness via proof-analysis results on derivable sequents. Finally, we obtain terminating tableaux calculi from these refutation display calculi. |
| title | Refutation calculi for lattice-based logics: from display to tableaux |
| topic | Logic Logic in Computer Science |
| url | https://arxiv.org/abs/2605.24717 |