Dmitry Rozplokhas

Input/Output (I/O) logic is a general framework for reasoning about conditional norms and/or causal relations. We streamline Bochman’s causal I/O logics via proof-search-oriented sequent calculi. Our calculi establish a natural syntactic link between the derivability in these logics and in the original I/O logics. As a consequence of our results, we obtain new, simple semantics for all these logics, complexity bounds, embeddings into normal modal logics, and efficient deduction methods. Our work encompasses many scattered results and provides uniform solutions to various unresolved problems.

We introduce a natural sequent calculus for preferential conditional logic PCL via embeddings into provability logic GL, achieving optimal complexity and enabling countermodel extraction. Extending the method to PCL with reflexivity and absoluteness – corresponding to Åqvist’s deontic system F with cautious monotony – we employ hypersequents to capture the S5 modality; the resulting calculus subsumes the known calculi for the weaker systems E and F within Åqvist family.

Preference-based deontic logics provide a foundation for normative reasoning but fail to distinguish between explicit allowances - specified by a designer - and implicit ones derived by inference. This distinction is crucial in systems where agents may act only if (explicitly or implicitly) permitted. In this paper, we formalize this inference by grounding the preference ordering over possible worlds in a permission base, i.e., a set of explicit allowances, and derive implicit permissions, as well as defeasible prohibitions and obligations. Our framework provides solutions to key deontic paradoxes and is a conservative extension of Åqvist’s dyadic deontic system F extended with cautious monotony. We illustrate the approach with a case study involving robotic agents operating under normative constraints and provide complexity results together with a QBF-based decision procedure to support automated reasoning.

Åqvist's logics (E, F, F+(CM), and G) are among the best-known systems in the long tradition of preference-based approaches for modeling conditional obligation. While the general semantics of preference models align well with philosophical intuitions, more constructive characterizations are needed to assess computational complexity and facilitate automated deduction. Existing small model constructions from conditional logics (due to Friedman and Halpern) are applicable only to F+(CM) and G, while recently developed proof-theoretic characterizations leave unresolved the exact complexity of theoremhood in logic F. In this paper, we introduce alternative small model constructions assembled from elementary building blocks, applicable uniformly to all four Åqvist's logics. Our constructions propose alternative semantical characterizations and imply co-NP-completeness of theoremhood. Furthermore, they can be naturally encoded in classical propositional logic for automated deduction.