The well-founded semantics (WFS) for logic programs yields a unique three-valued model that serves as an efficient core for skeptical reasoning, but lacks built-in mechanisms for choice and case-based reasoning, limiting its expressiveness for problems such as decision making and planning. Propositional SAT solvers excel at combinatorial problems like the latter but, unlike WFS, do not naturally support reasoning under incomplete information or encoding transitive closure properties. We present an integration of a choice operator into WFS that preserves the suitability of the semantics for scalable, partial-information reasoning. From a propositional perspective, our semantics gracefully captures semantically unassigned atoms and constraints; we illustrate this approach in a setting for reasoning about actions under uncertainty. Furthermore, classical propositional satisfiability can not only be embedded into our framework, but now also be extended with reasoning over transitive closures. In terms of program evaluation, we show that the choice operator can be materialized by a SAT solver while propagating the consequences of choices through an extension of the alternating fixpoint algorithm for WFS with conflicts that are propagated back to the SAT solver. To further increase computational performance, we develop clause learning and syntactic decomposition techniques for logic programs with choices.

Temporal Equilibrium Logic (TEL) extends Answer Set Programming (ASP) with linear-time temporal operators (LTL), enabling reasoning about dynamic systems. However, TEL enforces strong minimization criteria that may preclude intuitive models. Liveness formulas, for instance, tend to fail to have infinite equilibrium models, as TEL minimization postpones satisfaction forever. We address this limitation by introducing eager temporal operators (eager Until, eager Release, etc.), and present non-disjunctive temporal programs (NDTP) as a framework for modeling dependencies, inertia, and non-determinism. The fragment of tight temporal programs (TTP), which can be recognized efficiently based on automata techniques for loop detections, guarantees polynomial encodability into LTL. Practical examples, such as request-grant protocols and user permissions in distributed systems, illustrate the applicability of our approach.

The stable model semantics of logic programs has been characterized by Equilibrium Logic, which is a non-monotonic formalism that selects models from the (monotonic) intermediate logic of Here-and-There. It provides stable models for arbitrary propositional formulas and has been fruitfully extended to different modal languages. Among them are theories in the syntax of Linear-Time Temporal Logic (LTL), giving rise to Temporal Equilibrium logic (TEL) based on Temporal Here-and-There (THT). In TEL, models are selected that minimize truth among THT traces of the same length. In this paper, we consider a selection that in addition may reduce the number of transitions in a trace, intuitively forming a contraction of it. We thus introduce contracted THT and contracted TEL on top of a model selection on a logical basis. The resulting c-stable models can be viewed as stable models in TEL that can not be summarized into a smaller trace. We illustrate contraction on several examples related to logic programming and explore several properties, like the relation to TEL and LTL, and in particular the connection to the LTL property of stuttering.

In recent years, there has been growing interest in the application of temporal reasoning approaches and non-monotonic logics from artificial intelligence in dynamic systems that generate data. A well-known approach to temporal reasoning is the use of a progression technique, which allows for the online computation of logical consequences of a logical knowledge base over time. We consider a progression technique for Temporal Here and There and Temporal Equilibrium Logic, which is the logic underlying answer programming over linear-temporal logic (LTL). Compared to usual LTL online computation, where the goal is to check whether a trace is compliant with a temporal specification, our approach provides also the means to compute non-monotonic temporal reasoning over a trace of observations. Besides formal notions and results, we also present an algorithm for performing progression to monitor a dynamic system, which has been implemented as a proof of concept and allows for handling expressive application scenarios.

Abstract The continuous interest in Artificial Intelligence (AI) has brought, among other things, the development of several scenarios where multiple artificial entities interact with each other. As for all the other autonomous settings, these multi-agent systems require orchestration. This is, generally, achieved through techniques derived from the vast field of Automated Planning. Notably, arbitration in multi-agent domains is not only tasked with regulating how the agents act, but must also consider the interactions between the agents’ information flows and must, therefore, reason on an epistemic level. This brings a substantial overhead that often diminishes the reasoning process’s usability in real-world situations. To address this problem, we present ECHO, a hierarchical framework that embeds classical and multi-agent epistemic (epistemic, for brevity) planners in a single architecture. The idea is to combine (i) classical; and(ii) epistemic solvers to model efficiently the agents’ interactions with the (i) ‘physical world’; and(ii) information flows, respectively. In particular, the presented architecture starts by planning on the ‘epistemic level’, with a high level of abstraction, focusing only on the information flows. Then it refines the planning process, due to the classical planner, to fully characterize the interactions with the ‘physical’ world. To further optimize the solving process, we introduced the concept of macros in epistemic planning and enriched the ‘classical’ part of the domain with goal-networks. Finally, we evaluated our approach in an actual robotic environment showing that our architecture indeed reduces the overall computational time.