Guarded Open Answer Set Programming with Generalized Literals

We extend the open answer set semantics for programs with generalized literals. Such extended programs (EPs) have interesting properties, e.g. the ability to express infinity axioms – EPs that have but infinite answer sets. However, reasoning under the open answer set semantics, in particular satisfiability checking of a predicate w.r.t. a program, is already undecidable for programs without generalized literals. In order to regain decidability, we restrict the syntax of EPs such that both rules and generalized literals are guarded. Via a translation to guarded fixed point logic (μGF), in which satisfiability checking is 2-EXPTIME-complete, we deduce 2-EXPTIME-completeness of satisfiability checking in such guarded EPs (GEPs). Bound GEPs are restricted GEPs with EXPTIME-complete satisfiability checking, but still sufficiently expressive to optimally simulate computation tree logic (CTL). We translate Datalog LITE programs to GEPs, establishing equivalence of GEPs under an open answer set semantics, alternation-free μGF, and Datalog LITE. Finally, we discuss ω-restricted logic programs under an open answer set semantics.