基于布尔语义的Gentzen推导模型

来源：计算机科学与探索杂志2015年第2期北京时间：

作者：陈博，眭跃飞

单位：中国科学院 计算技术研究所 智能信息处理重点实验室，北京 100190

摘要：布尔模型是信息检索系统的一种基础模型。给出了命题逻辑和布尔代数间的一种新的对应关系，其中布尔代数中的不等式对应Gentzen系统中的矢列式，使得当一个不等式在任意布尔代数中为真，当且仅当它所对应的矢列式是可证的。并且使得在信息检索中，针对信息的推理可以有效地转为偏序集上的运算。讨论的命题逻辑语言的运算符为¬、∧、∨；并且定义了项（a|¬t|t1∧t2|t1∨t2,其中a是一个元素）来替代原先的公式和表示布尔代数中的元素。此外，定义了以布尔代数为论域的赋值v，将命题逻辑中的项赋值为布尔代数中的元素，并且如果∩t∈Γtv≤∪t∈Δtv，则矢列式Γ→Δ为真。最后给出了Gentzen系统下的可靠性和完备性定理的证明。

关键词：布尔代数,命题逻辑,不等式,完备性