Petri网用于Horn子句的逻辑推论

APPLICATION OF PETRI NETS TO LOGICAL INFERENCE OF HORN CLAUSES

这篇论文探索了命题逻辑的Horn子句的Petri网模型,求解逻辑推论Petri网模型的T—不变量是求解逻辑推论的核心步骤,本文提供了计算T—不变量的算法,这些算法基于归约的思想,另外,在算法中利用单字母规则、纯字母规则和割裂规则可提高算法的速度和简化算法的复杂性。

This paper studies Petri net models for the Horn clause form of propositional logic. Since finding the T-invariants of Petri net models of logical inference is the key step, the paper investigates the algorithms for computing such invariants. These are based on the idea of resolution, and exploit the presence of one-literal, pure -literal and splitting clauses to lead to faster computation.