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.

翻译：反驳演算是一种形式系统，用于推导给定逻辑中的无效公式。虽然反驳演算的概念在tableaux演算的发展中发挥了关键作用，但尚未有人尝试将反驳方法应用于显示演算。本文针对基本LE-逻辑（即规范地与任意符号的基本正规格扩张相关联的逻辑）引入了反驳显示演算。特别地，我们通过关于可推导矢列的证据分析结果证明了其可靠性和完备性。最后，我们从这些反驳显示演算获得了可终止的tableaux演算。