一种算子命题逻辑系统及其T-不变量推理算法

摘要

定义一种只带原子命题以及命题算子的算子命题逻辑,讨论了该逻辑的λ-归结的相容性、完备性及其若干逻辑性质。为了实现算子命题逻辑的归结推理,给出了算子命题逻辑的Petri网模型:Horn型,进一步讨论了推理算法:T-不变量算法,得到了算法的完备性定理。