We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polynomial-time equivalence checking that is sound with respect to Boolean algebra semantics. We generalize ortholattice reasoning and obtain an algorithm for proving a larger class of classically valid formulas. As the key result, we analyze a proof system for orthologic augmented with axioms. An important feature of the system is that it limits the number of formulas in a sequent to at most two, which makes the extension with axioms non-trivial. We show a generalized form of cut elimination for this system, which implies a sub-formula property. From there we derive a cubic-time algorithm for provability from axioms, or equivalently, for validity in finitely presented ortholattices. We further show that propositional resolution of width 5 proves all formulas provable in orthologic with axioms. We show that orthologic system subsumes resolution of width 2 and arbitrarily wide unit resolution and is complete for reasoning about generalizations of propositional Horn clauses. Moving beyond ground axioms, we introduce effectively propositional orthologic, presenting its semantics as well as a sound and complete proof system. Our proof system implies the decidability of effectively propositional orthologic, as well as its fixed-parameter tractability for a bounded maximal number of variables in each axiom. As a special case, we obtain a generalization of Datalog with negation and disjunction.

翻译：我们研究正义逻辑（orthologic）的证明理论与算法，该逻辑系统基于正义格（ortholattices），已在验证条件的简化与归一化中展现出实际应用价值。正义格弱化布尔代数结构，同时保持多项式时间等价性检查，且该检查对布尔代数语义是可靠的。我们将正义格推理进行泛化，得到一种用于证明更大一类经典有效公式的算法。作为核心结果，我们分析了带公理扩充的正义逻辑证明系统。该系统的重要特征在于将序列（sequent）中的公式数量限制至多两个，这使得公理扩充变得不平凡。我们证明了该系统的广义切割消去性质，由此得到子公式性质，并进一步推导出从公理可证性（等价于有限表示正义格中的有效性）的立方时间算法。我们还证明宽度为5的命题归结（propositional resolution）可证明正义逻辑加公理系统中的所有可证公式；该正义逻辑系统蕴含宽度为2的归结与任意宽度的单元归结，且对广义命题Horn子句推理具有完备性。突破基础公理，我们引入有效命题正义逻辑（effectively propositional orthologic），给出其语义及可靠完备的证明系统。该证明系统不仅证明有效命题正义逻辑的可判定性，还证明其在每个公理中最大变量数有界时的固定参数可解性。作为特例，我们得到带否定与析取的Datalog的泛化形式。