带公理的正交逻辑
Orthologic with Axioms
AI总结：
本文研究带公理的正交逻辑，通过限制相继式至多含两个公式的证明系统建立广义切消与三次时间可判定算法，并提出有效命题正交逻辑及其可靠完备系统。
摘要：
我们研究正交逻辑的证明论与算法。正交逻辑是一种基于正交格的逻辑系统，而正交格已在验证条件的化简和规范化方面展现出实际相关性。正交格弱化了布尔代数，同时具有相对于布尔代数语义可靠的多项式时间等价检查。我们推广了正交格推理，并得到一种用于证明更大一类经典有效公式的算法。\n作为关键结果，我们分析了一个增加公理的正交逻辑证明系统。该系统的一个重要特征是将相继式中公式的数量限制为至多两个，这使得加入公理的扩展并不平凡。我们证明了该系统的一种广义切消形式，并由此推出子公式性质。在此基础上，我们导出了一个三次时间算法，用于判定从公理出发的可证性，或者等价地，用于判定有限表示正交格中的有效性。我们进一步表明，宽度为5的命题归结可以证明带公理的正交逻辑中可证的所有公式。我们还表明，正交逻辑系统包含宽度为2的归结以及任意宽度的单元归结，并且对于命题Horn子句推广形式的推理是完备的。\n在基公理之外，我们引入了有效命题正交逻辑，给出其语义以及一个可靠且完备的证明系统。我们的证明系统蕴含有效命题正交逻辑的可判定性，并且当每条公理中变量的最大数量有界时，该问题具有固定参数易处理性。作为特例，我们得到了带否定和析取的Datalog的推广。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
