逻辑公式间的Jaccard 距离及其应用*

于 鹏

陕西科技大学 文理学院，西安 710021

1 引言

数理逻辑是研究推理的一门学科，它是现代数学的逻辑基础，也是人工智能与理论计算机的逻辑基础。在数理逻辑的研究中一直存在着两种研究方法——语构方法与语义方法。语构方法注重形式化推理，语义方法注重赋值计算。两者之间似乎存在着一种无形的隔离墙[1]。那么是否存在着一种有别于语构与语义的研究方法呢？文献[2-8]给出了肯定的回答。文献[2]在经典命题逻辑系统中利用均匀概率的思想引入了公式真度的概念，建立了计量逻辑学，给出了一种有别于语构语义的研究方法。随后文献[3-4]在Lukasiewicz 与R0多值逻辑系统中给出了相应命题逻辑系统的量化模型；文献[5]则将计量化方法引入到了多值模态逻辑中，建立了模态逻辑系统中的量化模型；文献[6]采用公理化方法给出了一类一阶谓词逻辑公式的公理化真度，将计量逻辑学引入到了一阶谓词逻辑中；文献[7-8]建立了概率计量逻辑学。这些研究成果的取得，为丰富非经典数理逻辑的研究做出了贡献[9-16]。

虽然计量逻辑学已经取得了丰硕的研究成果，但也存在如下问题：计量逻辑学中通过计算公式（φ→ψ）∧（ψ→φ）的真度来定义公式的相似度及伪距离的方法对于逻辑系统L、Łn、Ł*n、Łuk 与L*是适用的。但对于更为广泛的MTL（monoidal triangular norm based logic）逻辑系统却不再适用，这是因为对于一些左连续的t-模，构成伪距离的三角不等式不再成立。例如在[0，1]2上定义⊗算子如下：当时，a⊗b=0，当时，，可以验证⊗是左连续t-模，但不是强正则左连续t-模，通过⊗算子及其伴随的蕴涵算子，无法通过计量逻辑学的方法定义公式间的距离[17]。为了克服上述困难，文献[17-18]通过限制蕴涵算子是强正则蕴涵算子的方法，在MTL 逻辑中给出了一类特殊的MTL逻辑系统的真度理论，并称之为强MTL 逻辑系统（strong monoidal triangular norm based logic，SMTL），但这种改进不能从根本上克服上述不足。为了在更广泛的范围内建立并应用程度化推理方法，本文提出了一种基于Jaccard 相似系数的量化方法，这种方法不依赖于蕴涵算子的选取，可以直接通过赋值建立相应的逻辑度量空间，并研究其性质。通过推广本文方法，可以有效拓展计量逻辑的应用范围，为更好地研究理论计算机的逻辑基础提供助力。

2 公式间的Jaccard 距离

3 Jaccard 距离在刻画公式集结构中的应用

4 结束语

本文利用向量间的Jaccard 相似度与Jaccard 距离在经典逻辑系统中建立了以公式距离为核心概念的量化模型。讨论了逻辑度量空间中一些特殊集合的相容性问题，为探讨公式集F（S）的结构做出了尝试，得到了诸如矛盾式是（F（S），ρJ）中唯一的孤立点，并且每一个球形领域不相容等结论。本文研究结果的取得，为利用向量间的相似性度量来研究逻辑系统的性质提供了新的路径。那么在更为复杂的n值逻辑是否可以展开类似的讨论是后继的一个工作。