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.
| Subjects: | Logic (math.LO); Logic in Computer Science (cs.LO) |
| Cite as: | arXiv:2605.24717 [math.LO] |
| (or arXiv:2605.24717v1 [math.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2605.24717 arXiv-issued DOI via DataCite (pending registration) |
From: Andrea De Domenico [view email]
[v1]
Sat, 23 May 2026 20:13:31 UTC (79 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。