LEGO-like Small-Model Constructions for qvist's Logics

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, obtained uniformly for 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.