Ciabattoni, A., Olivetti, N., & Parent, X. (2022). Dyadic Obligations: Proofs and Countermodels via Hypersequents. In PRIMA 2022: Principles and Practice of Multi-Agent Systems. 24th International Conference, Valencia, Spain, November 16–18, 2022, Proceedings (pp. 54–71). Springer. https://doi.org/10.1007/978-3-031-21203-1_4
The 24th International Conference on Principles and Practice of Multi-Agent Systems (Prima 2022)
en
Event date:
16-Nov-2022 - 18-Nov-2022
-
Event place:
Valencia, Spain
-
Number of Pages:
18
-
Publisher:
Springer
-
Peer reviewed:
Yes
-
Keywords:
dyadic obligation; sequent calculus; search
en
Abstract:
The basic system 𝐄 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 𝐄 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 𝐄 and an effective countermodel computation in case of failure of proof search. By means of the refined calculus, we prove that validity in 𝐄 is Co-NP and countermodels have polynomial size.
en
Project title:
Axiomatisierung des Schließens mit normativen Konditionalen: M 3240-N (Fonds zur Förderung der wissenschaftlichen Forschung (FWF))
CC BY-NC-ND 4.0
