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

摘要：

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

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

分类号：TP18(自动化基础理论)

资助基金：The National Natural Science Foundation of China under Grant Nos.91224006,61173063,61035004,61203284,309737163

在线出版日期：2015-02-13（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：221-226