通过片段建模逻辑系统

本工作探讨了非经典逻辑的算法复杂性，聚焦于超直觉逻辑和模态系统。证明了命题逻辑通常可多项式时间归约至最多包含两个变量的片段（常归约至一个变量或甚至无变量片段）。此外，还证明了谓词逻辑通常可归约至包含一个或两个一元谓词字母和两个或三个个体变量的片段。该工作描述了实现此类归约的充分条件，并提供了失败的示例，确立了这些案例中的不可归约性。进一步地，本工作为Several逻辑提供了新的复杂度界限，关于谓词演算的Kripke不完备性结果，以及关于准谓词逻辑的经典Church和Trakhtenbrot定理的类比。