Goal-Directed Decision Procedures for Input/Output Logics

Input/Output (I/O) logics address the abstract study of conditional norms. Here, norms are represented as pairs of formulas instead of statements that themselves carry truth-values. I/O logics have been studied thoroughly in the past, including further applications and refinements. In this paper, a class of automated reasoning procedures is presented that, given a set of norms and a concrete situation, decide whether a specific state of affairs is obligatory according to the output operations of I/O logics. The procedures are parametric in the underlying logical formalism and can be instantiated with different classical objects logics, such as propositional logic or first-order logic. The procedures are shown to be correct, and a proof-of-concept implementation for propositional I/O logics is surveyed.