We comprehensively present a program of 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.

翻译：我们全面展示了一个通过约束代数的程序，将非经典逻辑的证明系统分解为其他逻辑（尤其是经典逻辑）的证明系统。也就是说，通过为另一种（通常是更简单的）逻辑的证明系统添加一个作为正确性条件的约束代数，来恢复目标逻辑的证明系统；例如，可以使用布尔代数在经典命题逻辑的相继式演算中给出约束，从而产生直觉主义命题逻辑的相继式演算。这种归约形式的背后思想是获得一个用于统一和模块化处理证明论的工具，并在语义逻辑与其证明论之间架起桥梁。本文讨论了该项目的理论背景，并提供了其在直觉主义逻辑和模态逻辑领域的几个应用实例。结果包括：对一大类命题逻辑的模块化无切割证明系统的统一处理；一种新的逻辑相对于模型论语义的可靠性与完备性方法的一般准则；以及一个从逻辑的证明论规范中推导出模型论语义的案例研究。