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

• 作者: 眭跃飞 陈博
• 来源期刊: 计算机科学与探索
• 学科: 工学
• 关键词: 布尔代数 命题逻辑 不等式 完备性
• 年，卷（期）: 2015,（2）
• 所属期刊栏目: 人工智能与模式识别
• 页码范围: 221-226
• 页数: 6页
• 分类号: TP18
• 字数: 4786字
• 语种: 中文
• DOI: 10.3778/j.issn.1673-9418.1409022

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈博	中国科学院计算技术研究所智能信息处理重点实验室	37	459	11.0	21.0
2	眭跃飞	中国科学院计算技术研究所智能信息处理重点实验室	35	313	9.0	17.0