ABSTRACT. Equilibrium Logic constitutes a well-established logical characterisation of Answer Set Programming (ASP) that has been recently extended to the deontic formalism called DELX. Focused on obligations of literals (built with explicit negation), DELX allows a certain degree of paraconsistency: a literal can be both obligatory and forbidden when one of those two norms is violated. This is convenient for contrary-to-duty situations, where a secondary obligation can co-exist with a contradictory, primary one when the latter is violated. Unlike modal approaches, any DELX theory can be reduced to a normal form where deontic operators are only applied on atoms. This allows a direct translation into ASP and was exploited in the recent tool for normative reasoning deolingo. However, the simplicity and flexibility of DELX comes at the price of its impossibility for a proper representation of disjunctive obligations like O(p ∨ q) that become DELX-equivalent to Op ∨ Oq. A similar problem arises with conjunctive prohibitions. In this paper, we study a modal deontic extension of equilibrium logic, MDEL, that avoids these problems by treating obligations as proper modal operators, while preserving the same restricted paraconsistency of DELX. We prove some basic properties of the new formalism and illustrate its use with several examples. Finally we prove that MDEL coincides with DELX for the syntactic fragment where modal operators are exclusively applied on explicit literals.

ABSTRACT. Equilibrium Logic is a logical characterisation of Answer Set Programming (ASP) that is very successfully used for the study of ASP foundations and extensions. One of such extensions is Temporal Equilibrium Logic (TEL), that allowed for incorporating temporal modal operators from Linear Temporal Logic (LTL) into ASP. Following the steps of Equilibrium Logic, TEL is defined by selecting models from a temporal extension of the intermediate logic of Here-and-There (HT). These models have the form of traces obtained by some kind of truth minimisation analogous to the one performed in non-temporal ASP. Recently, the variant called "contracted" TEL (cTEL) introduced an additional minimisation that may also shorten the length of the trace. Each contracted trace obtained with cTEL can be seen as a "summarisation" of a family of temporal stable models of a given theory. One irregularity of cTEL is that it is based on a variant of THT which, for non-temporal formulas, does not collapse to HT, but corresponds to a weaker intermediate logic instead. In this paper, we propose another variant of TEL, called "brief TEL" (bTEL), that performs a different trace length minimisation in which traces become shortest witnesses of the formula or theory. The new variant bTHT collapses to HT for non-temporal theories and it allows for applying Kamp's translation of temporal logic into Monadic First Order Logic, interpreting the obtained formulas under Quantified HT with dynamic domains. Specifically, we provide the bTEL definition, illustrate its effect on some examples, and prove that Kamp's translation is sound.

ABSTRACT. Answer Set Programming (ASP) is a well-known logic-based non-monotonic formalism enabling the representation of hard combinatorial problems in a natural and compact way. In ASP disjunction is particularly relevant, as it allows the modeling of problem in the second level of the Polynomial Hierarchy (PH). Recently, ASP(Q) has been introduced as an extension of ASP which allows the usage of quantifiers over answer sets of ASP programs. As a result, by alternating existential and universal quantifiers over different ASP programs, it becomes possible to model problems across the whole PH even without disjunction. Although ASP(Q) is supported by solid theoretical results and efficient implementations, there are still open theoretical questions to be addressed. One of these regard the computational cost introduced by disjunction within ASP(Q) programs. In this paper, we close this gap by providing complete complexity results for ASP(Q) programs with disjunction. Interestingly, we show that the presence of disjunction leads to only a limited increase in complexity.

ABSTRACT. Given an interpretation 𝐼 and a formula 𝜑 written in a logic 𝐿, the problem of model checking (MC) for 𝐿 is the problem of determining whether 𝐼 is a model of 𝜑. In this work, the computational complexity of MC for temporal equilibrium logic (TEL), a temporal extension of ASP, is investigated. The complexity of the universal and the existential variant of MC for TEL over Kripke structures, and of MC over linear traces, is determined. The complexity of these problems when the set of temporal operators, the temporal height or the implication height of the input formula is restricted is also determined.

ABSTRACT. The stable-unstable semantics of normal logic programs lifts their expressive power to cover decision problems from the second level of polynomial time hierarchy (PH). Under this semantics, each stable model of a main program is approved by oracle programs that are not supposed to have stable models given the stable model as input. If this idea is applied recursively, any level of PH can be reached with normal logic programs only, in analogy to quantified Boolean formulas (QBFs). In this article, we are interested in program development under stable-unstable semantics and verification problems that result from, e.g., the revision of programs. To create premises for formal verification in this setting, we introduce basic notions of equivalence for normal logic programs subject to stable-unstable semantics and study the computational complexity of the respective decision problems. Based on this analysis, we develop modular translations that enable the implementation of equivalence checking in practice, by using native answer set solvers for back-end reasoning tasks. Finally, we bridge the gap with respect to explicit quantification over stable models so that decisions about equi-coherence can be made using the method presented for stable-unstable semantics.

ABSTRACT. One avenue in the pursuit of increased trustworthiness and transparency of constraint satisfaction problem (CSP) solvers is that of step-wise explanations. A step-wise explanation bridges the gap between a CSP and a previously obtained solution to it through a series of logically valid reasoning steps that are “simple” enough for a human to understand and verify. In contrast, the reasoning techniques a solver might employ during solving are often highly optimized and “opaque”, i.e., hard to understand for non-experts. In prior work, the computational task of finding an explanation sequence has been reduced to finding certain kinds of cost-optimal unsatisfiable subsets, called OCUSs, of a set of boolean formulae. In this paper, we showcase how the recently proposed framework of answer set programming with quantifiers (ASP(Q)) can be used to compute such OCUSs and hence step-wise explanation sequences. We demonstrate this for the classic logic puzzle Sudoku and show how our declarative approach facilitates experimentation with various OCUS problem formulations. Finally, we empirically compare the ASP(Q) based approach with the previously proposed algorithms.