This work investigates the algorithmic complexity of non-classical logics, focusing on superintuitionistic and modal systems. It is shown that propositional logics are usually polynomial-time reducible to their fragments with at most two variables (often to the one-variable or even variable-free fragments). Also, it is proved that predicate logics are usually reducible to their fragments with one or two unary predicate letters and two or three individual variables. The work describes conditions sufficient for such reductions and provides examples where they fail, establishing non-reducibility in those cases. Furthermore, the work provides new complexity bounds for several logics, results on Kripke-incompleteness of predicate calculi, and analogues of the classical theorems of Church and Trakhtenbrot for the logic of quasiary predicates.
翻译:本研究探讨了非经典逻辑的算法复杂性,重点关注超直觉逻辑和模态系统。研究表明,命题逻辑通常可多项式时间归约至最多包含两个变量的片段(常可归约至单变量甚至无变量片段)。同时,证明了谓词逻辑通常可归约至仅含一至两个一元谓词字母及两至三个个体变量的片段。本文描述了此类归约的充分条件,并提供了归约失败的案例,确立了这些情况下的不可归约性。此外,研究为若干逻辑体系提供了新的复杂性界限,给出了谓词演算的克里普克不完全性结果,并针对拟元谓词逻辑建立了丘奇定理和特拉赫滕布罗特定理的类比形式。