SMT-Based Automated Reasoning for Åqvist’s Deontic Logics

Abstract

Åqvist's logics are an important and widely studied family within the field of deontic logics. Rozplokhas developed small model constructions for them, which transform arbitrary countermodels into equivalent models of bounded polynomial size. These constructions establish the co-NP-completeness of the theoremhood problem for all four Åqvist’s logics: E, F, F+CM, and G, and provide propositional encodings that enable efficient automated reasoning.In my thesis, I encoded Rozplokhas' constructions with the SMT solver Z3 to check the validity of formulas and to find minimal countermodels for invalid formulas. We present the entire workflow in detail: from parsing the input formulas, through the Z3-based encodings, to the structured representation of the countermodels.The tool provides three alternative ways of presenting countermodels: as plain text, as a matrix, or as a directed graph. All information can be displayed in a directed graph with straight, crossing-free edges for models with up to three worlds. For larger models, the preference relation is represented as a matrix and in plain-text form.As an additional optimization, we introduce simplification rules and procedures that reduce input formulas as much as possible, resulting in smaller encodings (by 55%) and a 77% reduction in formula size, which together lead to a speedup of 1.71 in solving times.As a case study, we applied the tool to analyse some well-known deontic paradoxes and check whether they are blocked in Åqvist's logics. Finally, we demonstrate the efficiency of the tool by performing runtime measurements on a generated test set of formulas and compare the results with an existing automated approach by Parent and Benzmüller based on Isabelle/HOL. Compared to their approach, our tool achieves up to a 25-fold speedup on invalid formulas, and supports all Åqvist’s logics rather than just the logic E. Its intuitive syntax and human-readable countermodel representations make our tool accessible to non-experts, positioning it as a lightweight and efficient alternative for future applications in automated deontic reasoning.