二元义务：通过超矢列进行证明与反模型构造
Dyadic obligations: proofs and countermodels via hypersequents
AI总结：
本文为二元道义逻辑系统 E 提出具有切割消除和子公式性质的超矢列演算，并据此给出判定程序、反模型构造及 Co-NP 复杂度上界。
摘要：
Åqvist 提出的二元道义逻辑基本系统 E 为反义务悖论提供了简洁解决方案，并能表示带有例外的规范。我们从证明论视角研究 E。我们提出一种具有良好性质的超矢列演算，其中最重要的是切割消除及其随之而来的子公式性质。该演算经过细化，可获得 E 的判定程序，并在证明搜索失败时有效计算反模型。利用细化后的演算，我们证明 E 中的有效性问题属于 Co-NP，且反模型具有多项式大小。
英文摘要：
The basic system E of dyadic deontic logic proposed by Åqvist offers a simple solution to contrary-to-duty paradoxes and allows to represent norms with exceptions. We investigate E from a proof-theoretical viewpoint. We propose a hypersequent calculus with good properties, the most important of which is cut-elimination, and the consequent subformula property. The calculus is refined to obtain a decision procedure for E and an effective countermodel computation in case of failure of proof search. Using the refined calculus, we prove that validity in E is Co-NP and countermodels have polynomial size.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
