Dyadic obligations: proofs and countermodels via hypersequents
<|reference_start|>Dyadic obligations: proofs and countermodels via hypersequents: The basic system E of dyadic deontic logic proposed by {\AA}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.<|reference_end|>
@article{ciabattoni2024dyadic,
    title={Dyadic obligations: proofs and countermodels via hypersequents},
    author={Agata Ciabattoni and Nicola Oliveti and Xavier Parent},
    journal={arXiv preprint arXiv:2406.09088},
    year={2024},
    doi={10.1007/978-3-031-21203-1_4},
    archivePrefix={arXiv},
    eprint={2406.09088},
    primaryClass={cs.LO}
}