Logic Programs with Ordered Disjunction: First-order Semantics and Expressiveness

ABSTRACT. Logic programs with ordered disjunction (LPODs) \cite{Brewka02} generalize normal logic programs by combining alternative and ranked options in the heads of rules. It has been showed that LPODs are useful in a number of areas including Game Theory, policy languages, planning and argumentations. In this paper, we extend propositional LPODs to the first-order case, where a classical second-order formula is defined to represent the stable model semantics of the underlying first-order LPODs. We then develop a progression semantics that is equivalent to the stable model semantics but naturally reflects the reasoning procedure of LPODs. We show that under finite structures, every LPOD can be translated into a first-order sentence, which provides a basis for computing stable models of LPODs. We further study the complexity and expressiveness of LPODs and prove that almost positive LPODs precisely capture normal logic programs, which indicates that ordered disjunction itself and constraints are sufficient to represent negation as failure.