Refutation calculi for lattice-based logics: from display to tableaux
Logic
2026-05-26 v1 Logic in Computer Science
Abstract
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.
Keywords
Cite
@article{arxiv.2605.24717,
title = {Refutation calculi for lattice-based logics: from display to tableaux},
author = {Andrea De Domenico and Giuseppe Greco and Alessandra Palmigiano and Mario Piazza and Andrea Sabatini},
journal= {arXiv preprint arXiv:2605.24717},
year = {2026}
}