LEGO-like Small-Model Constructions for {\AA}qvist's Logics

TL;DR

This paper introduces a unified, LEGO-like small model construction method for {e5}qvist's logics, providing new semantic characterizations, complexity results, and enabling automated deduction.

Contribution

It presents a novel, uniform small model construction approach applicable to all four {e5}qvist's logics, improving understanding of their semantics and computational complexity.

Findings

Proposes a LEGO-like small model construction for all four {e5}qvist's logics.

Establishes co-NP-completeness of theoremhood in these logics.

Enables encoding in propositional logic for automated deduction.

Abstract

{\AA}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 {\AA}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.