{"id":"arxiv/2605.24717","url":"https://arxiv.org/abs/2605.24717","tags":["math.LO","cs.LO"],"score":0,"title":"Refutation calculi for lattice-based logics: from display to tableaux","domain":"math.LO","source":"arxiv","authors":["Andrea De Domenico","Giuseppe Greco","Alessandra Palmigiano","Mario Piazza","Andrea Sabatini"],"reviews":0,"subject":"math.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-05-23","reactions":{}}