Humans are not bothered at all when it comes to choosing a way home among a plethora of alternatives. Similarly, in reasoning about action or planning, the underlying specifications admit an abundance of feasible plans. Among them, we usually find only a few reasonable alternatives while the majority bear an increasing number of redundancies, leading to infinite solutions in the worst case. Popular ways to counterbalance this are to extend the specification by objectives, like shortest plans, and/or imposing limits on the plan length. Both are often implemented with optimization procedures and/or incremental reasoning methods (extending insufficient plan lengths). However, computing a valid plan with such techniques usually involves solving numerous sub-problems of nearly the same scale as the actual problem — not to mention that solving somehow optimal plans is often particularly hard (due to phase transition phenomena). This rules out such techniques when it comes to highly demanding dynamic problems, as we witnessed in applications to robotic intra-logistics [14].

This motivates our approach to pair action theories with control theories in order to restrict our attention to plans selected by the control theory among all feasible ones induced by the action theory. This approach was pioneered by Levesque et al. in [20] by combining action theories in the Situation Calculus with control programs expressed in Golog. The rough idea is that a plan induced by an action theory must be compatible with a run of the associated Golog program. Although Golog’s design was inspired by Dynamic Logic [17], its semantics is given by a reduction to first-order logic. Unlike this, we developed in [3, 6] the foundations of an approach integrating Answer Set Programming (ASP [21]) with (linear) Dynamic Logic. More precisely, we are interested in the combination of the logic of Here-and-There (HT [19]) with linear Dynamic Logic over finite traces ([11]), called Dynamic logic of Here-and-There () and particularly its non-monotonic extension, Dynamic Equilibrium Logic ([6]). We review both logics in Section 2. ASP as such is known to constitute a fragment of Equilibrium Logic [22].

In what follows, our focus lies on implementing temporal and dynamic ASP via a reduction to regular ASP. This aligns with the above discussion insofar as temporal logic programs, featuring one step operators, are well-suited for providing action theories, while dynamic formulas allow for imposing compatibilities with path expressions, that amount to regular expressions over primitive actions.4 To this end, in this paper, we present the following contributions:

(i) we develop a three-valued characterization of (ii) we establish a normal form for showing that dynamic formulas can be reduced to (so-called) temporal logic programs; (iii) we use this reduction to implement a solver accepting dynamic formulas in

For (i), we extend the three-valued characterization from [16] to dynamic formulas, something that allows for greatly simplifying proofs and has thus benefits well beyond this paper. Also, it is, to the best of our knowledge, the first time this type of construction is used to capture dynamic logics and thus path expressions. This three-valued definition also allows for establishing (ii), which shows that any dynamic formula can be equivalently reduced to a syntactic fragment called temporal logic programs. This translation relies on the introduction of auxiliary atoms (in a Tseitin-style [25]) for, first, guaranteeing that its result is of polynomial size wrt the input formula, and, second, surmounting the fact that translations of dynamic into temporal formulas are usually impossible without extending the language. We explain both issues in more detail in Section 3. Finally, the great benefit of this reduction is that we can use it for (iii), that is, implementing dynamic formulas in , since temporal logic programs can be processed by an existing solver for temporal ASP, viz. telingo [8]. We describe the resulting implementation in Section 4 and show the potential impact of pairing action and control theories via an empirical analysis of an elevator scenario borrowed from [20].

We start from the syntax of Linear Dynamic Logic (LDL) defined in [11]. Given a set A of propositional variables (called alphabet), dynamic formulas path expressions are mutually defined by the pair of grammar rules:

This syntax is similar to the one of Dynamic Logic (DL [17]) but differs in the construction of atomic path expressions: while DL uses a different alphabet for atomic actions, in LDL there is a unique alphabet A (atomic propositions) and the only atomic path expression is the constant (read as “step”) that we also write as below), overloading the constant truth symbol. As we show further below, the above language allows us to capture several derived operators, like the Boolean and temporal ones:

All connectives are defined in terms of the dynamic operators . This involves the Booleans’ , among which the defi-nition of is most noteworthy since it hints at the implicative nature of . Negation is then expressed via implication, as usual in HT. Then, also allow defining the future temporal operators , standing for final, next, weak next, eventually, always, until, and release, and their past-oriented counterparts: . The weak one-step operators, , are of particular interest when dealing with finite traces, since their behavior differs from their genuine counterparts only at the ends of a trace. In fact, can also be expressed as ). A formula is propositional, if all its connectives are Boolean, and temporal, if it includes only Boolean and temporal ones. As usual, a (dynamic) theory is a set of (dynamic) formulas. Following the definition of linear DL (LDL) in [11], we sometimes use a propositional formula as a path expression actually standing for . This means that the reading of as a path expression amounts to just equivalent to , as we see below. Another abbreviation is the sequence of n repetitions of some expression and . For instance, which amounts to , as we see below.

the semantics, we start by defining a trace of length over alphabet A as a sequence . A trace is infinite if otherwise, that is, for some natural number . Given traces of length accordingly,

Although DHT shares the same syntax as LDL, its semantics relies on traces whose states are pairs of sets of atoms. A Here-and- There trace (for short HT-trace) of length over alphabet A is a sequence of pairs . As before, an HT-trace is infinite if otherwise. The intuition of using these two sets stems from HT and Equilibrium Logic: atoms in are those that can be proved; atoms not in are those for which there is no proof; and, finally, atoms in are assumed to hold, but have not been proved. We often represent an HT-trace as a pair of traces . The particular type of HT-traces that satisfy H = T are called total. Given any satisfaction of formulas, namely, , in terms of an accessibility relation for path expressions whose extent depends again on |= by double, structural induction.

Definition 1 (DHT satisfaction [6]) An length over alphabet A satisfies a dynamic formula at time point , if the following conditions hold:

where, for any is a relation on pairs of time points inductively defined as follows.

We see that quantify over time points i that are reachable via path expression from the current point k, that is,

dynamic theory to stand for the set of DHT models of length of a theory fine , that is, the whole set of models of of any length. When we just write

A formula . We call the logic induced by the set of all tautologies (Linear) Dynamic logic of Here-and-There (DHT for short). Two formulas are said to be equivalent, written . This allows us to replace and vice versa in any context, and is the same as requiring that is a tautology. Note that this relation, , is stronger than coincidence of models, viz. . For instance, because models are checked at the initial situation k = 0 and there is no previous situation at that point, so . However, in general, since is satisfied for any k > 0 (for instance instead). As with formulas, we say that path expressions equivalent, written

for any HT-trace M. The following equivalences of path expressions allow us to push the converse operator inside, until it is only applied to

Proposition 1 ([6]) For all path expressions and for all formulas , the following equivalences hold:

We say that converse normal form if all occurrences of the converse operator in are applied to

We now introduce non-monotonicity by selecting a particular set of traces that we call temporal equilibrium models. First, given an arbitrary set S of HT-traces, we define the ones in equilibrium as follows.

Definition 2 (Temporal Equilibrium/Stable models [6]) Let S be some set of HT-traces. A total rium trace of S iff there is no other

If is such an equilibrium trace, we also say that trace T is a stable trace of S. We further talk about temporal equilibrium or temporal stable models of a theory , respectively.

We write to stand for the temporal equilibrium models of respectively. Note that stable traces in and, thus, DEL is stronger than LDL. Besides, as the ordering relation among traces is only defined for a fixed , it is easy to see the following result:

Proposition 2 ([6]) The set of temporal equilibrium models of be partitioned by the trace length

(Linear) Dynamic Equilibrium Logic (DEL) is the non-monotonic logic induced by temporal equilibrium models of dynamic theories. We obtain the variants by applying the corresponding restriction to infinite or finite traces, respectively.

To illustrate non-monotonicity, take the formula:

whose reading is “keep sending an sos (s) while no help (h) is perceived.” Intuitively, behaves as a conditional referring to any future state after repetitions of checks whether h fails one more time at k = n: if so, it makes s true again. Without additional information, this formula has a unique temporal stable model per each length satisfying h is never concluded, and so, we repeat s all over the trace. Suppose we add now the formula becomes true after five transitions. Then, there is a unique temporal stable model for each satisfying:

Clearly, is not entailed any more (under temporal equilibrium models) showing that DEL is non-monotonic.

To conclude this section, we provide an alternative three-valued characterization of DHT that is particularly useful for formal elaborations involving auxiliary atoms. This alternative characterization relies on the idea of temporal three-valued interpretation in [4] for the case of TEL and is inspired, in its turn, in the characterization of HT in terms of G¨odel’s logic [16]. Under this orientation, we deal with three truth values {0, 1, 2} standing for: 2 (or proved true) meaning satisfaction “here”; 0 (or assumed false) meaning falsity “there”; and 1 (potentially true) that are formulas assumed true but not proved. Given an we define its associated truth valuations as a pair of mutually recursive functions that assign a truth value in the set {0, 1, 2} to formula at time point or to the pair (k, i) for path expression , respectively. The valuation of formulas follows the next rules:

whereas the function for path expressions is defined as follows:

This results in the following three-valued characterisation of HT-traces in

Theorem 1 Let -trace of length its associated valuation and

1. 2.

3. 4.

In this section, we elaborate upon a reduction of arbitrary dynamic formulas6 into a syntactic subclass called temporal logic programs [9]. A temporal logic program is a conjunction of temporal formulas with a restricted syntax that, when interpreted under temporal stable models, have a close relation to rules from disjunctive logic programming. Temporal logic programs were proved in [9] to constitute a normal form for (if we allow for auxiliary atoms) and used later on as a basic syntax for the temporal ASP system telingo [8]. We proceed next to describe their syntax.

Given a set of propositional variables A, we define the set of temporal literals as A temporal logic program is a set formed by three different types of rules:

An extended version of the paper with the proofs is available at

where (with are temporal literals in the case of dynamic rules and regular literals (i.e. ) in the case of initial and final rules. We also allow for global rules of the form that stand for the conjunction of an initial rule and a dynamic rule

Theorem 2 (Normal form) Every dynamic formula can be converted into a temporal program being -equivalent to

To prove the above theorem, we provide a sound transformation from any dynamic formula into a temporal logic program . As a first step, we assume that is already in converse normal form: this can be achieved by repeatedly applying the equivalences in Proposition 1. The reduction of into temporal program uses an extended alphabet that additionally contains new atoms (aka label) for formulas that are either subformulas of or elaborations of them. This set of formulas is called the Fisher-Ladner closure [12] of and formally defined below.

Definition 3 (Fisher-Ladner closure [12]) The Fisher-Ladner closure of a dynamic formula (in converse normal form) is a set of dynamic formulas inductively defined as follows:

Any set satisfying these conditions is called closed.

Proposition 3 For any dynamic formula , its closure nite.

Thus, given the dynamic formula on alphabet A to be translated, we define the extended alphabet convenience, we simply use or an atom

As happened with the normal form reduction for in [9], the translation is done in two phases: we first obtain a temporal theory containing double implications, and then we unfold them into temporal rules. We start by defining the temporal theory troduces new labels for each formula . This theory contains the formula and, per each label , a set of formulas fixing the label’s truth value. Formally:

Table 1 shows the definitions in the closure depending on the outer modality in the formula.

Table 1. Normal form translation

As an example, take the dynamic formula (which corresponds to the temporal formula p U q). In the first step, we get

where we just used q as its label stands for which belongs to . The truth of determined by which, in the table, is first unfolded into leading to:

with . Notice now that tains as a subformula, so it can be written as: just corresponds to the pair of formulas:

and the whole translation amounts to

As a second example, consider the formula ing that p holds in all even time points (this formula is well-known not to be LTL representable). The formulas obtained for

with is actually

As we have seen, in the general case, formulas in are not temporal rules, since they sometimes contain double implications. However, they all have the forms inner propositional formula formed with temporal literals. For instance, in (2), the inner corresponds to the propositional formula . As first shown in [7] propositional formulas in HT can be reduced to conjunctions of disjunctive rules. In this way, we can apply HT transformations (as those in [10]) and THT axioms [1] to eventually obtain a temporal logic program. In the case of (2), the inner double implication is unfolded into three rules that, after applying property , eventually lead to:

Given an , we define its restriction to alphabet . Similarly, for any set S of HT-traces we write to stand for S} as expected.

The following lemma shows that are equivalent:

Lemma 1 Let be a dynamic formula over being associated with the three-valuation m.

Theorem 3 For any dynamic formula and any length

for any arbitrary dynamic formula

Proposition 4 Translation has a polynomial size with respect to the size of

with dynamic formulas over finite traces. More precisely, the current version supports negated occurrences of dynamic formula, as in integrity constraints; it is available at https://github.com/potassco/telingo/releases/tag/v2.0.0.

To this end, telingo provides (theory) atoms of form ‘that encapsulate arbitrary dynamic formulas . Their syntax is given in Table 2; it is supplied as a theory grammar to the underlying ASP system clingo [13].8 The one of the dynamic operators follows that of , respectively, by extending ‘by prepending path expressions separated by a dot, viz. ‘and ‘’ . For instance, the dynamic formula Section 3 is expressed as

The current restriction to negated dynamic formulas allows for an easier algorithmic treatment since formulas in the scope of negation are interpreted as in (just as negated formulas in HT can be treated as in classical logic). Although this restriction will be lifted in

3{wait; up; down; serve} = 1 :- not &final. 4:- up, at(X), not floor(X+1). 5:- down, at(X), not floor(X-1).

12:- called(X), &final.

14ready :- called(X), at(X).

16#program initial.

18:- not &del{ *( (*up + *down) ;; ?ready ;; serve) 19;; *wait .>? &final }.

a next release, it already supports an agreeable modeling methodol- ogy for dynamic domain separating action and control theories. The idea is to model the actual action theory with temporal rules, fixing static and dynamic laws, while the control theory, enforcing certain (sub)trajectories, is expressed by integrity constraints using dynamic formulas. This is similar to the pairing of action theories in situation calculus and Golog programs [20].

Let us illustrate this with the example in Listing 1 that aims at modeling a simple elevator. This example is borrowed from [20]. The temporal program in Lines 1-14 constitutes the action theory; it is expressed in . All its rules in the scope of the program declaration headed by always are thought of as being preceded by they are added as global rules (see beginning of Section 3). Line 3 tells us that exactly one of the four actions wait, up, down, or serve, occurs at any time before the end of the trace. The next two lines check the preconditions of action up and down. Lines 7-9 provide effect and inertia axioms for the fluent at, which reflects the current floor of the elevator. Line 10 expresses that a call at a floor persists unless the floor was served. Line 12 gives the actual goal condition, requiring that no call remains unserved in the final state. Line 14 indicates that the elevator is ready to serve, whenever it is at a floor that it was called to.9

The integrity constraint in Line 18-19 represents the following dynamic formula:

The purpose of this constraint is to eliminate fruitless wandering of the elevator. More precisely, it provides a simple control theory stipulating that the elevator must pick one direction, either up or down, and move in this direction until it reaches a floor to which it was called, and serve this floor; this process is repeated an arbitrary number of times; finally, the elevator may have to wait until the end of the trace. Note that (13) is posed as an initial temporal rule, as indicated by the program directive in Line 16. Hence, its path expression must be matched by a trajectory from the initial to the final state, enforced by F in (13) and &final in Line 19 in Listing 1, respectively.

For computation, programs as in Listing 1 are treated according to the translation introduced in Section 3. That is, at the outset, all dynamic formulas are transformed into temporal rules. Each dynamic formula is recursively rewritten using translation until the for-

Table 2. Past and future temporal operators in telingo and their counterparts

mula is free of any dynamic constructs. This is accomplished via clingo’s functionalities for manipulating abstract syntax trees. Then, telingo’s API allows us to turn the obtained equivalences among temporal formulas directly into a regular logic program. This involves the extension of predicates with time variables as well as the introduction of variables and rules reflecting the successive lengthening of finite traces (cf. [8]; temporal rules are treated analogously). This is needed to be able to solve temporal logic programs incrementally. That is, traces of increasing length are investigated by incrementally extending the underlying logic program. Once a model is found, the search stops and the corresponding traces are provided as output. This amounts to computing a nonempty set stable traces for the smallest and some temporal program P at hand.

Finally, let us examine the impact of the dynamic formula in Listing 1 on the trajectories induced by the action theory as well as solver performance. Although we believe that (13) allows us to significantly reduce the number of trajectories induced by the action theory in lines 1-14, its impact on search is less clear cut because it comes with an augmentation of the number of constraints in the solver.

To analyze this, we consider the following simple elevator problems: We look at n = 5, 7, 9, 11 floors, respectively, and initially place a call at the ground and top floor while the elevator sits on the middle floor. The goal is to have all floors served at the end of a trace (cf. Line 12). This can be expressed by the following facts.

We run each instance with different horizons, beginning with the minimum lengths of satisfiable traces, viz. , and gradually extending this by 1 to 4 to introduce more room for redundancies. Our experiments were run with telingo 2-and obtained without imposing any time or memory restrictions. Our results are summarized in Table 3. Each entry, a/c, contrasts statistics obtained from the pure action theory in Line 1-14, viz. a, with the combination of action and control theory in Line 1-19, c.

For each setting, we give the number of traces, number of choices during search, and the number of constraints in the solver (after all translations, preprocessing etc.). First of all, we notice that the addition of (13) yields exactly two valid traces, no matter what setting is considered. In the first trace, the elevator goes first up all the way and then straight down, and vice versa in the second trace. Both traces are actually minimal as witnessed throughout the first column. This is because the elevator is placed at the mid floor, otherwise one would be shorter than the other. Next, we observe how drastically the number of trajectories and the underlying search increases for the action theories with each extension of the horizon. For instance, for 11 floors and an horizon of 19 (11+5+4) the mere action theory admits 200900 valid traces, among which only two are conformant with (13). Looking at the underlying search, it is amazing how radically (13) trims the search, in that only nine choices are needed to find the two traces. This is also astonishing since its addition led to an increase from 7042 to 9026 constraints in the solver. Similar yet less extreme observations can be made in all remaining settings.

To get an idea on runtime, we conducted the same experiment on the larger instance with 71 floors (=107), since the ones obtained for 5 to 11 floors are negligible. Finding the first model without the dynamic constraint takes 19.4 sec, including 17.8 sec of solving, while adding the dynamic constraint yields a runtime of only 2.2 sec with 0.01 sec of solving. As with filtering traces, it seems that the dynamic constraint greatly contributes to guiding the solver.

Clearly, our empirical analysis is rather limited and can only indicate the potential impact of dynamic formulas on reducing search efforts for finite traces. Nonetheless, we observe that adding the dynamic formula in (13) not only (sometimes drastically) reduces the number of feasible traces but also significantly cuts down the number of choices despite its non-negligible increase of the resulting problem.

We have elaborated upon the computational foundations of the Dynamic logic of Here-and-There and its equilibrium traces, viz. and [6], in order to design and implement an expressive ASP system for modeling and solving dynamic domains. Our approach was motivated by the methodology of separating action and control theories, similar to what is done in Situation Calculus and Golog [20].

To this end, we carved out a normal form for dynamic formulas in that consists of its fragment corresponding to temporal logic programs. The translation of dynamic formulas into normal form heavily relies on the introduction of auxiliary variables. This allows us to keep the size of the resulting temporal program polynomial in that of the original formula. And moreover it allows us to overcome the common intranslatability of dynamic into temporal formulas when keeping the same language. Our proof of the normal form result relies on a novel characterization of in terms of a three-valued logic.

Table 3. Summary of experimental results in the elevator domain

The reduction of dynamic formulas to temporal logic programs enabled us to implement dynamic expression on top of the temporal ASP solver telingo. Since it constitutes a true extension of the ASP system clingo, we obtain a full-fledged modeling language extended by temporal and dynamic constructs. We provided a limited empirical analysis demonstrating the potential impact of using dynamic formulas to select traces among the ones induced by an associated temporal logic program. This is how we see the interaction of control and action theories in our framework.

To the best of our knowledge, telingo provides the first ASP system augmented with constructs from dynamic and temporal logics. Encodings for bounded model checking in LTL over infinite traces were given in [18]. This was extended to certain action theories expressed with dynamic operators in [15]. A key feature of these encodings is to capture loops inducing infinite traces. This is avoided in [5], where infinite traces in TEL are captured by B¨uchi automata via model checking. Encodings of Golog in ASP were proposed in [24, 23]. This amounts to directly implementing a filter on traces, as done in Listing 1, without any logical underpinnings. In [6], we provided a different translation from converse-free dynamic formulas in to propositional formulas in HT, which themselves can be translated into an equivalent disjunctive logic program (cf. [10]). More precisely, a dynamic formula is translated in [6] into a logic program . This translation differs from the current one, in several aspects. First, the target language is different: while produces a temporal logic program, directly obtains a propositional logic program corresponding to some fixed time point i. This is because is thought for using telingo as a backend, along with its incremental solving mode, whereas was thought for the direct use of a specific trace length. Thus, the advantage of that it does not pass through temporal expressions from telingo as an intermediate step. On the other hand, its disadvantages are that cannot contain the converse operator and that can be exponential, since it makes use of distributivity for normalization both of path expressions and of formulas into logic programs. Note that is applicable to any arbitrary dynamic formula and takes polynomial time and space. Its main disadvantage is that, in the general case, the resulting temporal logic program may not be amenable for incremental ASP computation. To do so, an extra condition is required: (non-constraint) temporal rules must additionally be present-centered, that is, conditions may refer to the past or present of head expressions, but not to their future. In the general case, not satisfy this requirement: for instance, one of the directions of (10) yields the rule , so the head depends on a condition in its future. Fortunately, in the case of negated formulas , as the ones currently implemented in telingo, this limitation does not apply, since we can exclusively use constraints for the translation. Our future work aims at a full integration of dynamic formulas into ASP and thus telingo. In particular, we will study the more general case in which dynamic expressions can be used in non-constraint rules. As we did for temporal theories and the so-called past-future form (see [6]), we plan to identify a similar syntactic condition for a dynamic formula so the resulting temporal program is guaranteed to be present-centered. It will be interesting to experiment with encodings deriving dynamic formulas rather than merely testing them.

This work was partially supported by Ministry of Science and Innovation, Spain (grant TIC2017-84453-P), Xunta de Galicia, Spain (grants GPC ED431B 2019/03 and 2016-2019 ED431G/01, CITIC Research Center).

[1] P. Balbiani and M. Di´eguez, ‘Temporal here and there’, in Proceedings of the Fifteenth European Conference on Logics in Artificial Intelligence (JELIA’16), pp. 81–96. Springer, (2016).

[2] Proceedings of the Fifteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’19). Springer, 2019.

[3] A. Bosser, P. Cabalar, M. Di´eguez, and T. Schaub, ‘Introducing temporal stable models for linear dynamic logic’, in Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR’18), pp. 12–21. AAAI Press, (2018).

[4] P. Cabalar, ‘A normal form for linear temporal equilibrium logic’, in Proceedings of the Twelfth European Conference on Logics in Artificial Intelligence (JELIA’10), pp. 64–76. Springer, (2010).

[5] P. Cabalar and M. Di´eguez, ‘STELP — a tool for temporal answer set programming’, in Proceedings of the Eleventh International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’11), pp. 370–375. Springer, (2011).

[6] P. Cabalar, M. Di´eguez, and T. Schaub, ‘Towards dynamic answer set programming over finite traces’, In [2], pp. 148–162.

[7] P. Cabalar and P. Ferraris, ‘Propositional theories are strongly equivalent to logic programs’, Theory and Practice of Logic Programming, 7(6), 745–759, (2007).

[8] P. Cabalar, R. Kaminski, P. Morkisch, and T. Schaub, ‘telingo = ASP + time’, In [2], pp. 256–269.

[9] P. Cabalar, R. Kaminski, T. Schaub, and A. Schuhmann, ‘Temporal answer set programming on finite traces’, Theory and Practice of Logic Programming, 18(3-4), 406–420, (2018).

[10] P. Cabalar, D. Pearce, and A. Valverde, ‘Reducing propositional theories in equilibrium logic to logic programs’, in Proceedings of the Twelfth Portuguese Conference on Artificial Intelligence (EPIA’05), pp. 4–17. Springer, (2005).

[11] G. De Giacomo and M. Vardi, ‘Linear temporal logic and linear dynamic logic on finite traces’, in Proceedings of the Twenty-third International Joint Conference on Artificial Intelligence (IJCAI’13), pp. 854–860. IJCAI/AAAI Press, (2013).

[12] M. Fischer and R. Ladner, ‘Propositional dynamic logic of regular programs’, Journal of Computer and System Sciences, 18(2), 194–211, (1979).

[13] M. Gebser, R. Kaminski, B. Kaufmann, M. Ostrowski, T. Schaub, and P. Wanko, ‘Theory solving made easy with clingo 5’, in Technical Communications of the Thirty-second International Conference on Logic Programming (ICLP’16), OASIcs, pp. 2:1–2:15. (2016).

[14] M. Gebser, P. Obermeier, T. Otto, T. Schaub, O. Sabuncu, V. Nguyen, and T. Son, ‘Experimenting with robotic intra-logistics domains’, Theory and Practice of Logic Programming, 18(3-4), 502–519, (2018).

[15] L. Giordano, A. Martelli, and D. Theseider Dupr´e, ‘Reasoning about actions with temporal answer sets’, Theory and Practice of Logic Programming, 13(2), 201–225, (2013).

[16] K. G¨odel, ‘Zum intuitionistischen Aussagenkalk¨ul’, Anzeiger der Akademie der Wissenschaften in Wien, 65–66, (1932).

[17] D. Harel, J. Tiuryn, and D. Kozen, Dynamic Logic, MIT Press, 2000.

[18] K. Heljanko and I. Niemel¨a, ‘Bounded LTL model checking with stable models’, Theory and Practice of Logic Programming, 3(4-5), 519–550, (2003).

[19] A. Heyting, ‘Die formalen Regeln der intuitionistischen Logik’, in Sitzungsberichte der Preussischen Akademie der Wissenschaften, 42– 56, Deutsche Akademie der Wissenschaften zu Berlin, (1930).

[20] H. Levesque, R. Reiter, Y. Lesp´erance, F. Lin, and R. Scherl, ‘GOLOG: A logic programming language for dynamic domains.’, Journal of Logic Programming, 31(1-3), 59–83, (1997).

[21] V. Lifschitz, Answer Set Programming, Springer, 2019.

[22] D. Pearce, ‘Equilibrium logic’, Annals of Mathematics and Artificial Intelligence, 47(1-2), 3–41, (2006).

[23] M. Ryan, ‘Efficiently implementing GOLOG with answer set programming’, in Proceedings of the Twenty-Eighth National Conference on Artificial Intelligence (AAAI’14), pp. 2352–2357. AAAI Press, (2014).

[24] T. Son, C. Baral, T. Nam, and S. McIlraith, ‘Domain-dependent knowledge in answer set planning’, ACM Transactions on Computational Logic, 7(4), 613–657, (2006).

[25] G. Tseitin, ‘On the complexity of derivation in the propositional calculus’, Zapiski nauchnykh seminarov LOMI, 8, 234–259, (1968).

Proposition 5 The valuations of derived formulas and path expressions correspond to:

Proof of Proposition 1. By induction on the complexity of the formula. For the cases of , note that

• ⟨• ⟨

For the case of a propositional variable p, it is easy to check that

For the modal operators, we need to proceed by double induction.

• Case

– Item 1: From left to right, if so duction we get 2. Therefore, satisfaction relation we get

Conversely, if then, by definition, there exists fore, both . By induction, . By the satisfaction relation, Therefore,

– Item 2: From left to right, if there exists By induction we get (three-valued) satisfaction relation we get

From right to left, if then there exists . From this we conclude that . By induction . By the satisfaction relation we get

• Case

– Item 1: From left to right, assume by contradiction that . Therefore there exists such that imp2. By definition, . We consider all cases:

∗ If . By induction on we get that From the satisfaction relation we get contradiction.

∗ By induction hypothesis . Therefore,

From right to left, let us assume by contradiction that and let us consider the following cases:

∗ There exists induction . Therefore, imp. By definition, fore : a contradiction.

∗ There exists induction . Therefore, imp. From this it follows that By the satisfaction relation we get contradiction.

– Item 2: From left to right, assume by contradiction that . Therefore . This means that there exists such that imp. By induction on

conclude that satisfaction relation it follows : a contradiction.

From right to left, assume by contradiction that . Therefore, there exists . By induction, 0. This means that impAs a consequence, : a contradiction.

In order to prove items 3 and 4 we proceed by induction on

– Item 3: from left to right, if Therefore, . Conversely, if j = k + 1. By definition,

– Item 4: from left to right, if Therefore, . Conversely, if then j = k + 1. By definition

– Item 3: from left to right, if . By induction on lows that . Conversely, if . By induction on

– Item 4: from left to right, if . By induction on . Conversely, if and . By induction on so

– Item 3: from left to right, if then either By induction on fore . Conversely, if then . By induction hypothesis we get that either so

– Item 4: from left to right, if then either By induction on fore . Conversely, if then . By induction on we get that either

– Item 3: from left to right, if exists . By induction we get that . Therefore

2. By definition . Conversely, if then there exists that . This means that . By induction hypothesis . By definition

– Item 4: from left to right, if exists . By induction we get that . Therefore 0. By definition . Conversely, if then there exists that . This means that . By induction hypothesis . By definition

• : We proceed by induction on n in its turn. For n = 0 we have that Suppose proved it up to equivalent to:

by structural induction for and induction on n this is equivalent to:

The case for is analogous.

QED

Proposition 6 The following expressions are

Proof of Lemma 3. Take the whose three valued interpretation

for any formula and for all is an atom , which implies that both valuations coincide for atoms, and so, remains to be shown that , which is equivalent to

The first satisfaction relation follows directly from the definition of and we had that is a model of . For the second part, we consider the following cases depending on the structure of the subformula

1. For we have two formulas in

• For the formula , the equivalence must be satis-fied for any being trivial). Then,

• For the second formula, we get the following

Note on the other side that, . Therefore,

2. For we have two formulas in . For the formula we refer the reader to the case of second formula, , we present the proof below:

3. For : we have two formulas in

- For the formula note that the prefix that the double implication must be satisfied for any and, moreover, that this is trivially true when have to prove may assume n > 0. The proof can be obtained as follows:

- For satisfying the formula , this is the same than requiring and this follows from

4. For we have two formulas in . For the formula we refer the reader to the case of the second formula, , note that definition.

5. For amounts to proving . In this case we have that

6. For we have that and so, amounts to proving . In this case we have

7. For

8. For amounts to proving case we have

9. For amounts to proving

10. For amounts to proving

• For the formula amounts to show that

• For the formula the proof amounts to prove that . We show this below.

• For the formula amounts to show that

• For the formula , we refer the reader to the previous case (but using (19) instead).

QED Proof of Lemma 1. We proceed by structural induction on

- If we use the second formula in . It follows that

- If we can apply the first formula in guarantees particular, we can take j = k and so:

3. If , we consider two cases

• : on one side we take the second formula of to conclude that and, by definition,

• if we refer the reader to the previous case.

4. If we divide into two cases:

5. we distinguish two cases

- k = 0 we use the second formula in to conclude that

6. If . Note that, by definition, . Moreover, it follows that

7. If . Note that, by definition, . Moreover, it follows that

8. If , let us take

We can apply the induction hypothesis on . Therefore we obtain

9. If , let us take

We can apply the induction hypothesis on . Therefore we obtain

10. If , let us consider . Note that . For this proof we will assume that , which is equivalent to the assumption the translation to can be directly replaced by the one of

11. If , let us consider . Note that . For this proof we will assume that , which is equivalent to the assumption the translation to can be directly replaced by the one of

12. For , we distinguish two different cases depending on k

• if we use the second formula in to conclude

• if , let us take . By defini-tion . Therefore, . With this we can use the first formula in as follows:

13. For , we distinguish two different cases depending on k

• if we use the second formula in to conclude

• if , let us take . By defini-tion . Therefore, . With this we can use the first formula in as follows:

QED