We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof system for a target logic by enriching a proof system for another, typically simpler, logic with an algebra of constraints that act as correctness conditions on the latter to capture the former; for example, one may use Boolean algebra to give constraints in a sequent calculus for classical propositional logic to produce a sequent calculus for intuitionistic propositional logic. The idea behind such forms of reduction is to obtain a tool for uniform and modular treatment of proof theory and provide a bridge between semantics logics and their proof theory. The article discusses the theoretical background of the project and provides several illustrations of its work in the field of intuitionistic and modal logics. The results include the following: a uniform treatment of modular and cut-free proof systems for a large class of propositional logics; a general criterion for a novel approach to soundness and completeness of a logic with respect to a model-theoretic semantics; and, a case study deriving a model-theoretic semantics from a proof-theoretic specification of a logic.

翻译：我们提出一个综合性研究纲领，运用约束代数方法分析非经典逻辑的证明系统如何分解为其他逻辑（尤其是经典逻辑）的证明系统。具体而言，通过为目标逻辑的证明系统附加一个约束代数结构——该结构作为后者的正确性条件——可以从另一通常更简单的逻辑证明系统重构目标逻辑的证明系统。例如，在经典命题逻辑的矢列演算中引入布尔代数约束，即可构建直觉主义命题逻辑的矢列演算。这类归约方法的核心思想在于：为证明论的统一模块化处理提供工具，并在逻辑语义学与其证明论之间建立桥梁。本文探讨了该项目的理论背景，并通过直觉主义逻辑与模态逻辑领域的若干实例展示其有效性。研究成果包括：为大规模命题逻辑族提供模块化且免切的证明系统统一处理方法；建立衡量逻辑相对于模型论语义的可靠性与完备性的新型通用判据；以及从逻辑的证明论规范推导出其模型论语义的案例研究。