Lattice Logic Properly Displayed
Lattice Logic Properly Displayed
复制标题
正确显示晶格逻辑
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
A. Palmigiano
中科院分区：
文献类型：
--
作者：
G. Greco;A. Palmigiano
本文给出了（非分配）格逻辑的一个合理的、完备的、保守的、具有割消和子公式性质的显示演算。适当性（即在规则中所有参数部分的统一替换下的封闭性）是本提案的主要兴趣和附加值，并且允许最平滑的Belnap式切割消除证明。我们的建议建立在格逻辑的语义环境的代数和序理论的分析，并适用于显示演算的设计中的多类型的方法学的指导方针。
We introduce a proper display calculus for (non-distributive) Lattice Logic which is sound, complete, conservative, and enjoys cut-elimination and sub-formula property. Properness (i.e. closure under uniform substitution of all parametric parts in rules) is the main interest and added value of the present proposal, and allows for the smoothest Belnap-style proof of cut-elimination. Our proposal builds on an algebraic and order-theoretic analysis of the semantic environment of lattice logic, and applies the guidelines of the multi-type methodology in the design of display calculi.