Encoding Definitional Fragments of Temporal Action Logic into Logic Programming Marc van Zee1 , Patrick Doherty2 , and John-Jules Meyer3 1 Department of Individual and Collective Reasoning, University of Luxembourg 2 Department of Computer and Information Science, Linköping University 3 Department of Information and Computing Science, Utrecht University Abstract. Temporal Action Logics (TAL) is an expressive class of nonmono- tonic temporal logics for reasoning about action and change. In previous work, it has been shown that a very general fragment of the logic can be reduced to first- order logic with equality. Consequently, standard theorem proving techniques can be used to reason in TAL. TAL is intended to be used for robotics. In this case, standard theorem proving techniques are too general and do not provide efficient decision procedures. The goal of this article is to identify a limited subset of TAL that can be directly mapped to a normal logic program. Although quite restric- tive, this sets the lower bound on what can be done with direct mappings to logic programs. Discussions concerning extensions to the restricted fragment are also provided. 1 Introduction Temporal Action Logics (TAL) [2, 4] is a general class of nonmonotonic temporal log- ics for reasoning about action and change that are based on the Features and Fluents framework of Sandewall [13]. TAL is highly expressive and includes the use of context- dependent durative actions, durational fluents (fluents with default values), ramification constraints, qualification constraints, concurrent and non-deterministic actions. Like several other action formalisms, TAL uses circumscription [10, 11] to solve the frame and the ramification problems, which require nonmonotonicity. In [2], it was shown how the 2nd-order circumscription component could be reduced to a logically equiva- lent 1st-order component using quantifier elimination. Consequently, standard theorem proving techniques can be used to reason with TAL. This is problematic from an effi- ciency perspective since in the case of many domains such as robotics, one requires an efficient decision procedure to answer queries. VITAL4 was an early implementation of a fragment of TAL that uses model generation techniques. This does not scale for large TAL narratives though. 4 http://www.ida.liu.se/∼jonkv/vital 2 Marc van Zee, Patrick Doherty, and John-Jules Meyer The generality of TAL is useful in other domains as a natural semantic specifica- tion language. For instance, it provides a formal specification of TALplanner. TALplan- ner5 [3, 6] is an award-winning forward-chaining planner based on TAL. Both TAL planner and an execution monitoring framework based on TAL have been used in Un- manned Aerial Vehicles [5], developed at Linköping University.6 In this paper, the focus is on isolating a restricted fragment of TAL and showing that it can be encoded in a sound manner into normal logic programs. Unfortunately, the fragment for which this works is highly restrictive. The subset of TAL narratives with deterministic single step actions and complete information about initial state can be encoded soundly into logic programs. This in fact makes sense, since any non- determinism in TAL narratives must be excluded from such a direct mapping. Relaxing the single step constraint and complete information at initial state both result in intro- ducing non-determinism and thus multiple minimal models. This, in fact, would apply to any alternative action formalism. The systematic use of logic programming as a basis for soundly implementing frag- ments of action formalisms was introduced in the case of the Situation Calculus by Reiter (see [12], Chapter 5). The initial fragment identified by Reiter had similar restric- tions for progression to work. This article applies the techniques introduced by Reiter to encode a fragment of TAL soundly into logic programs and analyzes the feasibility of extending the technique to more general fragments of TAL. An algorithm is developed for the systematic translation of definitional theories of TAL into logic programs. The definitional fragment of TAL identified is called TALM. It is then shown that extending this fragment via the use of direct encodings into normal logic programs is not feasible. Any attempt to generalize the TALM fragment results in the introduction of non-determinism into the fragment. The main limitation here is the inability to encode a unique values axiom for features in TAL narratives. This im- mediately rules out non-deterministic actions, actions with duration and an incomplete initial state. The rest of this paper is organised as follows: In Section 2 we introduce the basic concepts of TAL, in Section 3 we develop an algorithm to translate definitional theories into logic programs, in Section 4 we reformulate a constrained TAL theory, TALM, as a definitional theory, and finally in Section 5 we discuss the limitations of the translation. 2 Temporal Action Logics Due to lack of space, we refer the reader to [4] for details about the full syntax and semantics of TAL. In this section, we summarize the main components necessary for understanding the techniques introduced. In TAL, a scenario (or narrative) can be described in a compact surface language L(ND), which is a high-level macro expandable language consisting of action type specifications (acs), dependency constraints (dep), domain constraints (dom), persis- tence statements (per), observation statements (obs), and action occurrence statements 5 http://www.ida.liu.se/divisions/aiics/aiicssite/projects/talplanner.en.shtml 6 http://www.ida.liu.se/divisions/aiics/aiicssite/index.en.shtml Encoding Definitional Fragments of Temporal Action Logic into Logic Programming 3 (occ). To make sure that fluents will not be persistent when they are changed by an action, the reassignment macro R can be used. R([t2 ]α) ensures that α will hold at the time point t2 . Consider the following scenario due to Reiter [12] that will be used as a running example. Example 1 (Simple robot specification). There is one robot called rob and there are two objects, namely a ball and a vase. A robot can only pick up an object if he is not holding anything and if he is next to the object, and he can only drop an object if he is holding it. When a robot drops an object it will fall on the floor. Initially, rob is next to vase and not next to ball. Rob is not holding anything. First, rob picks up vase, after which he walks to ball and drops vase. The narrative specification of this example in the macro language L(ND) is: acs1 [t1 , t2 ] pickup(r, o) ; [t1 ] ∀o1 [¬holding(r, o1 )] ∧ nextto(r, o) → R([t2 ] holding(r, o) ∧ ¬onfloor(o)) acs2 [t1 , t2 ] walk(r, o) ; R([t2 ] nextto(r, o)) ∧ ∀o1 [o 6= o1 → R([t2 ] ¬nextto(r, o1 ))] acs3 [t1 , t2 ] drop(r, o) ; [t1 ] holding(r, o) → R([t2 ] ¬holding(r, o) ∧ onfloor(o)) obs1 [0] nextto(rob, vase) ∧ ¬nextto(rob, ball) obs2 [0] ∀z ¬holding(rob, z) obs3 [0] onfloor(vase) ∧ onfloor(ball) occ1 [0, 1] pickup(rob, vase) occ2 [1, 2] walk(rob, ball) occ3 [3, 4] drop(rob, vase) Reasoning about a narrative in L(ND) is done by translating it into the base lan- guage L(FL)), which is an order-sorted classical first-order language using a linear, discrete time structure. The language uses the ternary predicates Holds and Occurs, and the binary predicate Occlude. The translation from L(ND) to L(FL) is given by the function T rans [4]. For instance, T rans([t]f =ω) ˆ is defined as Holds(t, f, ω). Sim- ilarly, T rans(R((t, t0 ]f =ω)) ˆ is defined as ∀t00 (t < t00 < t0 → Occlude(t00 , f )) ∧ Holds(t0 , f, ω). Occlude(t, f ) represents that a persistent or durational fluent f is ex- empt from inertia or default value assumption, respectively, at time t. T rans([t, t0 ]Ψ ), where Ψ is an action term, is defined as Occurs(t, t0 , Ψ ), which represents that action Ψ occurs in the interval [t, t0 ]. Consider any narrative N and let Nper , Nobs , Nocc , Nacs , Ndomc , and Ndepc denote the sets of persistence statements, observation statements, action occurrence statements, action type specifications, domain constraints, and dependency constraints in N respec- tively. The TAL domain description (referred to as preferred narrative) ∆N is given by CIRC[Γocc ; Occurs] ∧ CIRC[Γdepc ∧ Γacs ; Occlude] ∧ Γf nd ∧ Γtime ∧ Γper ∧ Γobs ∧ Γdomc , where Γper , Γobs , Γocc , Γacs , Γdomc , and Γdepc are the formulas in L(FL) (first-order logic formulas) obtained by applying T rans on N , Nobs , Nocc , Nacs , Ndomc , and Ndepc 4 Marc van Zee, Patrick Doherty, and John-Jules Meyer respectively; Γf nd is the set of foundational axioms in L(FL), containing unique name axioms, unique value axioms, etc., and Γtime is the axiomatization of the particular temporal structure used in TAL. By proposition 18.2 in [4], the circumscription of Occurs and Occludes, respec- tively CIRC[Γocc ; Occurs] and CIRC[Γdepc ∧ Γacs ; Occlude], can be transformed into first-order definitional forms either through quantifier elimination of predicate com- pletion techniques. Example 2 (Robot Specification, Ctd.). The following is a representation of acs1 in the language L(FL): acs1’ Occurs(t1 , t2 , pickup(r, o)) → ∀o1 [¬Holds(t1 , holding(r, o1 ), true)] ∧ Holds(t1 , nextto(r, o), true) → Occlude(t2 , holding(r, o)) ∧ Occlude(t2 , onfloor(o))∧ Holds(t2 , holding(r, o), true) ∧ ¬Holds(t2 , onfloor(o), true). The circumscription of the Occurs predicate in the action occurrences (occ1, occ2, and occ2) above is equivalent to the following first-order formula: Occurs(t1 , t2 , a) ↔(t1 = 0 ∧ t2 = 1 ∧ a = pickup(rob, vase))∨ (t1 = 1 ∧ t2 = 2 ∧ a = walk(rob, ball))∨ (t1 = 2 ∧ t2 = 3 ∧ a = drop(rob, vase)) The circumscription of the Occlude predicate in the action specifications (acs1, acs2, and acs3) above is equivalent to the following set of first-order formulas: Occlude(t, holding(rob, o)) ↔ o = vase ∧ ∀o1 [¬Holds(0, holding(r, o1 ), true)]∧ Holds(0, nextto(r, o), true) ∧ 1 ≤ t ≤ 2 Occlude(t, nextto(rob, o)) ↔ o = ball ∧ t = 2 Occlude(t, onf loor(o)) ↔ o = vase ∧ (t = 1 ∧ ∀o1 [¬Holds(0, holding(rob, o1 ), true)]∧ Holds(0, nextto(rob, o), true) ∨ t = 3 ∧ Holds(2, holding(rob, o), true) 3 def2P Algorithm: From Definitional Theories to Logic Programs We begin by providing some background definitions and techniques for the sake of completeness. Although these techniques are well-known by now, we state them here for completeness and readability of the paper. 3.1 Negation As Failure Semantics: Clark’s Completion The most widely accepted declarative semantics for negation as failure is the “com- pleted database” introduced by Clark [1]. This is now usually called the completion or Clark completion of a program P and denoted by comp(P ). We shall define this only Encoding Definitional Fragments of Temporal Action Logic into Logic Programming 5 when P is what Lloyd calls a normal program, i.e. a set of clauses (not containing the predicate =) of the form A ← L1 , . . . , L m where A is an atom and L1 , . . . , Lm are literals. To avoid tedious repetition we shall assume that all programs referred to are normal. Similarly goals and queries will be as- sumed to be normal, i.e. of the forms ← L1 , . . . , Lm , and ? − L1 , . . . , Lm , respectively. Norms logic programs generally does not use classical negation, but negation as failure. This means exactly what it says: if some fact cannot be derived from the theory (i.e. it fails), then we assume that the negation of this fact can be derived from the the- ory (i.e. it succeeds). One of the most widely applicable and often used semantics for negation as failure was given by Clark [1]. This is usually called the (Clark) completion, comp(P ), of the original program P . The idea of this result is that we use the ’implied iff’: we simply replace all the implications of the normal program clauses with equiv- alences. The basic result of Clark is that negation as failure is sound for comp(P ) for both success and failure. Because of the syntactical form of normal program clauses, comp(P ) will be a definitional theory. 3.2 Lloyd-Topor Transformations Although Clark’s theorem assumes that a Prolog program P can be obtained from the theory T by writing the if-halves, it does not give any details on how this is done. Be- cause Prolog only uses disjunctions and conjunctions as connectives, we will translate the other connectives (implication, bi-implication and quantifiers) into a form such that it is amenable for a Prolog interpreter. The same can be said for the query goals. The Lloyd-Topor transformations [9, 8] is a set of derivation rules for systematically transforming if-halves of definitions of the syntactic form W → A into a syntactic form suitable for implementation as Prolog clauses. Here, A must be an atomic formula, but W may be an arbitrary first-order formula, possibly involving quantifiers, in which case we require that the quantified variables of W be different from one another, and from any of the free variables mentioned in W . Originally, the Lloyd-Topor transformations introduce auxiliary predicates when transforming negated existential quantifiers and disjunctions, but Reiter [12] shows that these predicates are only introduced for expo- sition of the results of Lloyd-Topor and that they can be omitted using a process called unfolding. The output of these revised transformations is a single Prolog executable formula lt(W ) → A, without introducing new predicates and clauses. Here, lt(W ) is a formula Reiter defines inductively on the syntactic structure of W . It is defined as follows: 1. If W is a literal: lt(W ) = W . 8. lt(¬¬W ) = lt(W ). 2. lt(W1 ∧ W2 ) = lt(W1 ) ∧ lt(W2 ). 9. lt(¬(W1 ∧ W2 )) = lt(¬W1 ) ∧ lt(¬W2 ). 3. lt(W1 ∨ W2 ) = lt(W1 ) ∨ lt(W2 ). 10. lt(¬(W1 ∨ W2 )) = lt(¬W1 ) ∨ lt(¬W2 ). 4. lt(W1 → W2 ) = lt(¬W1 ∨ W2 ). 11. lt(¬(W1 → W2 )) = lt(¬(¬W1 ∨ W2 )). 5. lt(W1 ≡ W2 ) = lt((W1 → W2 ) ∧ 12. lt(¬(W1 ≡ W2 )) = lt(¬(W1 → W2 ) ∧ (W2 → W1 )). ¬(W2 → W1 ))). 6. lt((∀x )W ) = lt(¬(∃x )¬W ). 13. lt(¬(∀x )W ) = lt((∃x )¬W ). 7. lt((∃x )W ) = lt(W ). 14. lt(¬(∃x )W ) = ¬lt(W ). 6 Marc van Zee, Patrick Doherty, and John-Jules Meyer 3.3 Allowed Programs Clark’s theorem is not applicable to any Prolog interpreter, but only to proper Prolog interpreters. Such an interpreter is one that evaluates a negative literal not A, using negation as failure, and moreover, does so only when (at the time of evaluation) the atom A is ground. When A is not ground, the interpreter may suspend its evaluation, working on other literals until A does become ground, or it may abort its computation. Either way, it never tries to fail on non-ground atoms, because this can result in unsound behaviour [12]. Due to space limitations, we leave out the details7 , but we instead intro- duce a well-known class of programs that is known to be complete, meaning that it will not cause problems with floundering [14], namely the allowed programs. In Section 4 we show that every TALM theory results in an allowed Prolog program. Definition 1 (Allowed Program, Allowed Query). A query is said to be allowed if every variable which occurs in it occurs in a positive literal of it; a program clause A ← L1 , ..., Ln is allowed if every variable which occurs in it occurs in a positive literal of its body L1 , ..., Ln and a program is allowed if all of its clauses are allowed. 3.4 the def2P algorithm The contents of the previous section can be summarized into a single algorithm that translates a definitional theory to a Prolog program. Definition 2 (def2P algorithm). The def2P algorithm takes a definitional theory T as input and output a Prolog program def2P(T ) by performing the following steps: 1. T is augmented with Clark’s Equality Axioms [1], obtaining T 0 , 2. T 0 is translated into Lloyd-Topor Normal Form, obtaining Tnorm 0 , 0 3. The if-halves of the definitions of Tnorm form the Prolog program P , 4. If P falls in the class of allowed programs, return P . Else, return false. The following result follows directly from the previous discussion. Theorem 1 (Completeness of def2P algorithm). The Prolog resolution algorithm for def2P(T ) is complete for the theory T . 4 A Definitional Theory for TAL We constrain TAL to integer and positive time, relational and inertial fluents, complete initial state and deterministic, single-step and non-overlapping actions. Moreover, we omit symbolic constants, dependency constraints and domain constraints. Finally we assume a consistent narrative specification. Call this constrained formalism TALM. 7 For a more detailed discussion see [15], Section 3.2.2. Encoding Definitional Fragments of Temporal Action Logic into Logic Programming 7 Definition 3 (TALM theory). A TALM theory is a constrained TAL theory Γ = Γobs ∧ Γocc ∧ Γacs ∧ Γper ∧ Γf nd of the form: Γobs Holds(t, f, v) for t ∈ N, fluent f and value v ∈ {true, false} Γocc Occurs(t, t + 1, a) for t ∈ N and action a Γacs Occurs(t, t + 1, a) → Φ(t, t + 1) Γper ¬Occlude(t + 1, f ) → Holds(t + 1, f, v) ≡ Holds(t, f, v) Γf nd UNA, CWA, Unique values axioms We obtain a definitional theory for this restricted narrative by providing a definition for the three predicates in the base language L(FL): Occurs, Occlude and Holds. Occurs: By definition, only positive occurrences of Occurs predicates are allowed in Γocc . Each such atomic formula can be put in the logically equivalent form ∀t1 ,t2 ,a (t1 = ut ∧t2 = u0t ∧a0 = a(u)) → Occurs(t1 , t2 , a0 ). Denote such a formula by ∀t1 ,t2 ,a0 Ψi → Occurs(t1 , t2 , a0 ) where Ψi = (t1 = u ∧ t2 = u0t ∧ a0 = a(u)). Then the conjunction of ground atomic formulas can be put in the following form: ∀t1 ,t2 ,a0 (Ψ1 ∨Ψ2 ∨...∨Ψn ) → Occurs(t1 , t2 , a0 ). Denote this formula by ∀t1 ,t2 ,a Υ → Occurs(t1 , t2 , a). By proposi- tion 18.2 in [4], in this case circumscription is equivalent to predicate completion, i.e. CIRC(Γocc ; Occurs) is equivalent to: ∀t1 ,t2 ,a Υ ≡ Occurs(t1 , t2 , a). (1) Occlude: Circumscribing Occlude works in a similar way. The predicate Occlude oc- curs only in the postcondition of dependency constraints and actions specification for- mulas. Each member of Γacs and Γdep can be transformed syntactically into the logi- cally equivalent form ∀t,f Γi (t, f ) → Occlude(t, f ). Again, by proposition 18.2 in [4], CIRC(Γacs ∧ Γacs ; Occlude) is equivalent to: k _ ∀t,f [ Γi (t, f )] ≡ Occludes(t, f ) (2) i=1 Holds: We obtain the definition of the Holds predicate using case distinctions. The following proposition simplifies the TALM narrative. Proposition 1 (Redundant observations at t > 0). Observations that occur at t > 0 in TALM can be inferred from actions and can thus be removed from the narrative. Proof. Let Γ be some narrative specification in TALM. Let Γ 0 be the narrative Γ with all observations at t > 0 removed. We have to show that Γ and Γ 0 have the same models, i.e. Γ ⇔ Γ 0 . The truth value of Occurs and Occlude is equivalent for both narratives, because these predicates do not occur in the observations. This means that it suffices to show that Γ |= Holds(t, f, v) ⇔ Γ 0 |= Holds(t, f, v) for any time point t, fluent f and valuation v. ”⇒”: Suppose for some time point t, fluent f and valuation v ∈ {true, false} we have that Γ |= Holds(t, f, v). We have to show that Γ 0 |= Holds(t, f, v). Suppose that Holds(t, f, v) is not an observation, it follows now directly that Γ 0 |= Holds(t, f, v), 8 Marc van Zee, Patrick Doherty, and John-Jules Meyer because the only difference between Γ and Γ 0 are observations. Suppose to the contrary that Holds(t, f, v) is an observation. Now, if there is no action specification that implies Holds(t, f, v), then this observation follows from the persistence statement as well, otherwise it will be contradicting with it and the narrative is inconsistent. Therefore, the observation is redundant. On the other hand, if there is an action specification formula that implies Holds(t, f, v), then since the action specification formulas are unchanged in Γ 0 , it follows that Γ 0 |= Holds(t, f, v). ”⇐”: Follows directly from the fact that Γ 0 is a subset of Γ , meaning that everything that is valid in Γ 0 will be valid in Γ . Now, to obtain a definition for the Holds predicate, suppose some time point t, fluent f and value v. – Suppose t = 0. The only formulas that can assign a value to the Holds predicate at t = 0 are observations, because at time point 0 no actions can occur since an action has a minimal duration of 1 and a minimal starting time of 0. Moreover, all fluents are assigned a value through the observations because TALM has a complete initial state. So, given that t = 0, " n # _ ∀f,v f = Pi (ui ) ∧ v = vi ≡ Holds(t, f, v). (3) i=1 – Suppose t > 0. We introduce a second case distinction on Occlude: • Suppose ¬Occlude(t, f ). Using the persistence statement (see Definition (3)) we obtain ∀v Holds(t, f, v) ≡ Holds(t − 1, f, v). So, given that t > 0 and ¬Occlude(t, f ), Holds(t − 1, f, v) ≡ Holds(t, f, v) (4) • Suppose Occlude(t, f ). By Eq. (2) we obtain Γi (t, f ). Because actions are deterministic and non-overlapping, and because there will be no observations (Proposition 1) there will be a unique action specification formula that is now true and implies a single Holds statement for the fluent f . Using this we obtain Holds(t, f, v). This means that, given that t > 0 and Occlude(t, f ), (Γi (t, f ) ∧ v = vi ) ≡ Holds(t, f, v) (5) We now state the completion theorem of the Holds predicate: Theorem 2 (Completion of Holds). Formulas (3), (4) and (5) provide necessary and sufficient conditions for the predicate Holds: " k # _ t=0∧ f = Pj (ui ) ∧ v = vi ∨ i=1 t > 0 ∧ (¬Occlude(t, f ) ∧ Holds(t − 1, f, v)∨ Occlude(t, f ) ∧ Γi (t, f ) ∧ v = vi ) ≡ Holds(t, f, v) (6) Encoding Definitional Fragments of Temporal Action Logic into Logic Programming 9 Proof. Formulas (3), (4) and (5) are the only formulas that make the Holds predicate true in a TALM narrative. We obtain the definition directly by putting these formulas in a disjunction and adding the conditions for each case. Fortunately, it turns out that every definitional theory of a TALM narrative fall into the class of allowed programs of Definition 1. We show this in the following theorem. Theorem 3 (Allowed program). Suppose Γ is a TALM narrative , which is translated into a definitional theory by using the equivalences above. Let P be the program that is obtained from this theory by applying Clark’s Theorem. P falls into the class of allowed programs. That is, every variable that occurs in a rule in P occurs in a positive literal of the body of the rule. Proof. We have to show that each program clause in P is an allowed program clause. Each clause corresponds to a predicate of the theory, which means that we will have to consider Occurs, Occlude, and Holds. By definition, all literals occurring in the definition of Occurs are positive [4]. This is the same for the definition of Occlude predicate, because the only literals that occur in this definition are Holds literals, and each negated Holds predicate can be translated into an equivalent positive one, us- ing the equivalence Holds(t, f, true) ≡ ¬Holds(t, f, false). Finally, there occurs one negation in the definition of the Holds predicate, which is in the scope of the Occlude predicate (see Theorem 2): . . . t > 0 ∧ (¬Occlude(t, f ) ∧ Holds(t − 1, f, v) ∨ . . .) ≡ Holds(t, f, v) The variables occurring in the negative literal are t and f , which both occur posi- tively in the Holds predicate that directly follows it. Therefore, Holds is an allowed clause too, because all variables occurring in a negative literal occur in a positive literal in the body. We will now demonstrate the translation of our running example. We invite the reader to download the application that was developed along with this paper called TALTrans- lator. This application can perform the transformation automatically and comes with a user-friendly GUI and several examples8 . Example 3 (Robot specification, continued). The definition of the Holds predicate for the fluent onfloor is (slightly simplified for readability): Holds(t, onf loor(o), v) ↔ t = 0 ∧ v = true∨ t > 0∧ (o = vase ∧ (t = 1 ∧ ∀o1 [Holds(0, holding(rob, o1 ), f alse)]∧ Holds(0, nextto(rob, o), true) ∧ v = false∨ t = 3 ∧ Holds(2, holding(rob, o), true) ∧ v = true)∨ ¬Occlude(t, onfloor(o)) ∧ Holds(t − 1, onfloor(o), v)) 8 Download from http://icr.uni.lu/marc/TALTranslator.rar 10 Marc van Zee, Patrick Doherty, and John-Jules Meyer Next, we input this definitional theory into the def2P algorithm (Def. 2). Since Prolog provides the equality axioms (step 1), we can directly apply the Lloyd-Topor transfor- mations. What follows is the Prolog code for the fluent onfloor(o) (note that Prolog uses ”;” for disjunction): holds(T,onfloor(O),V) :- T=0, V=true ; T>0, ( O=vase, T=1, holds(0, holding(rob,O1),false), holds(0,nextto(rob,O),true), v=false; t=3, holds(2, holding(rob,O), true), v=true); not occlude(T, onfloor(O)), T2 = T-1, holds(T2, onfloor(O),V) ). 5 Relaxing the Constraints In the previous sections we have introduced a restricted fragment of TAL, which we referred to as TALM. We then showed how it can be translated into a logic program sound for the narrative in question. In this section we will consider if, and to what extent the constraints on TALM can be relaxed while still being able to use direct mappings of TAL narratives into logic programs. We discuss non-deterministic actions, concurrent actions, actions with duration and an incomplete initial state. Almost all the restrictions that we will discuss (except for concurrent actions) have one property in common: relaxing each of them will result in a non-deterministic narrative. This means essentially that a narrative can have multiple interpretations. The unique values axioms associated with the foundational axioms in TAL for any narrative are crucial when discussing non-deterministic narratives, because it rules out narratives in which a fluent has two values at the same time point. This implies that rather than modelling several alternative values for a fluent in one mode, several mini- mal models are required instead. The unique values axioms follow: ∀t,f ∃v Holds(t, f, v) (7) ∀t,f,v1 ,v2 [v1 6= v2 ⊃ ¬(Holds(t, f, v1 ) ∧ Holds(t, f, v2 ))] (8) In the previous section we did not explicitly encode these axioms into the definitional theory, because each narrative in TALM is fully deterministic: it will have a unique model in which each fluent has exactly one value. Satisfaction of the axioms is implicit in the encoding of TALM narratives into a logic program. Theorem 4 (Unique Model). Each TALM narrative Γ has a unique model m in which each fluent has exactly one value per time point. Proof. We show that for each narrative Γ in TALM, the interpretations of the predicates Holds, Occlude and Occurs are unique. Because these are the only predicates occur- ring in the narrative, it follows directly that the narrative has a unique model. Suppose some narrative Γ , – For Occurs: The interpretation of Occurs is determined only by the action occur- rences. This interpretation is unique because the assignments of the action occur- rences are non-deterministic and non-overlapping. Encoding Definitional Fragments of Temporal Action Logic into Logic Programming 11 – For Occlude: Similar to Occurs. – For Holds: This follows directly from the case distinction used when constructing the definition of the Holds predicate (see Section 2). 5.1 Extending TALM with Non-determinism Any relaxation of the restrictions on TAL narratives associated with TALM introduce one form or another of non-deterministic choices of fluent values at time points. This implies that in the general case, Theorem 4 no longer holds. For any relaxation of TALM to be sound relative to encoding into a logic program, the unique values axioms would have to become an explicit part of the the definitional theory. Unfortunately, this is not possible. Observe that Equation 8 is equivalent to, v1 6= v2 → ¬Holds(t, f, v1 ) ∨ ¬Holds(t, f, v2 ), It is in general not possible to bring such a formula into a definitional form. To obtain a definition of a predicate P , we require a set of formulas of the form, (Φ1 → P ) ∧ ... ∧ (Φi → P ), which can then be combined to (Φ1 ∨ ... ∨ Φi ) → P . Unfortunately the unique values axiom does not provide us with such a construc- tion, and we can also not transform it in a direct manner into one. This means that we cannot hope to express the unique values axiom and at the same time maintain a transformation to an equivalent definitional theory. Therefore, we generally cannot allow non-deterministic actions in TALM, because it will possibly lead to an inconsis- tent model in which a fluent has two values at one time point. This immediately rules out the possibility to extend TALM with any form of non-determinism, including non- deterministic actions, multi-step actions, and an incomplete initial state, because each of these extensions introduce a form of non-determinism into the theory. This is not surprising as it applies to most any approach to modelling action and change. 5.2 Concurrent actions Much work in reasoning about action and change has been done under the assumption that there is a single agent performing sequences of non-overlapping actions. The use of explicit time points in TAL enables the direct specification of narratives where action execution intervals are partly or completely overlapping, whether those actions are per- formed by a single agent or by multiple agents. No special concurrency operators are required to do this. Independent Concurrent Actions: Extending TALM with independent concurrent ac- tions involving disjoint sets of features is unproblematic. Since the effects of the actions do not interfere with each other (i.e. two actions change the same fluent at the same time), the expected effects will take place. Such concurrent actions will not introduce 12 Marc van Zee, Patrick Doherty, and John-Jules Meyer multiple models. We omit the proof of this proposition because it is trivial. The conse- quence of this is that the unique value axioms can be omitted, which means that it is possible to extend TALM with independent concurrent actions. Dependent Concurrent Actions: In the case where actions affecting the same fluents occur concurrently, concurrent actions that affect the value of the same fluent can never assign different values to this fluent, because this would lead to an inconsistent narrative. Otherwise, both actions assign the same value to the fluent. In either case, it is not necessary to add the unique values axioms to the theory because there are no multiple models introduced. Again, the proof of this is trivial and is omitted. Thus, concurrent actions are allowed as long they do not assign different values to the same fluent at the same time. Or in other words: concurrent actions that assign different values to the same fluent are not allowed. 6 Conclusion The aim of this paper was to isolate a definitional fragment of the highly expressive TAL formalism and show how it can be soundly encoded into a normal logic program. This was done by defining the fragment TALM and providing an algorithm, def2P, that encodes TAL narratives in this fragment into logic programs that can be shown to be sound and complete relative to this particular fragment. One would of course like to find more general reasoning techniques that relax some of the restrictions associated with TALM narratives. At the very least, one would require a mapping to disjunctive logic programs such as Answer Set Programs. Lee and Palla [7] have recently demon- strated that it is possible to reformulate more general fragments of TAL into an answer set program. Consequently the SAT-based implementation techniques used there can be applied to TAL. One of the authors is currently looking into the translation of TAL the- ories to Satisfiability Module Theory (SMT) programs. Another appropriate extension would include the use of constraints to more efficiently model the temporal constraints associated with more general TAL narratives. 7 Acknowledgments Marc van Zee is funded by the National Research Fund, Luxembourg. References 1. Clark, K.L.: Negation as failure. In: Logic and Databases. pp. 293–322 (1977) 2. Doherty, P.: Reasoning about action and change using occlusion. In: 11th European Confer- ence on Artificial Intelligence,1994. John Wiley and Sons (1994) 3. Doherty, P., Kvarnström, J.: Talplanner : A temporal logic based forward chaining planner. Annals of Mathematics and Artificial Intelligence 30(1-4), 119–169 (2000) 4. Doherty, P., Kvarnström, J.: Temporal action logics. In: Handbook of Knowledge Represen- tation, pp. 709–757. No. 3 in Foundations of Artificial Intelligence, Elsevier (2009) Encoding Definitional Fragments of Temporal Action Logic into Logic Programming 13 5. Doherty, P., Kvarnström, J., Heintz, F.: A temporal logic-based planning and execution moni- toring framework for unmanned aircraft systems. Autonomous Agents and Multi-Agent Sys- tems 19(3), 332–377 (Dec 2009) 6. Kvarnström, J.: TALplanner and other extensions to Temporal Action Logic. Ph.D. thesis, Linkping UniversityLinkping University, Department of Computer and Information Science, The Institute of Technology (2005) 7. Lee, J., Palla, R.: Reformulating temporal action logics in answer set programming. In: AAAI 2012 (2012) 8. Lloyd, J.W.: Foundations of logic programming. Springer-Verlag New York, Inc. (1987) 9. Lloyd, J., Topor, R.: Making prolog more expressive. Journal of Logic Programming 1, 225– 240 (1984) 10. Mccarthy, J.: Circumscription—a form of non-monotonic reasoning. Readings in nonmono- tonic reasoning pp. 145–152 (1987) 11. McCarthy, J.: Applications of circumscription to formalizing common sense knowledge. Ar- tificial Intelligence 59, 23–26 (1986) 12. Reiter, R.: Knowledge in action: logical foundations for specifying and implementing dy- namical systems. MIT Press, Cambridge, Mass. (2001) 13. Sandewall, E.: Features and fluents (vol. 1): The representation of knowledge about dynam- ical systems. Oxford University Press, Inc., New York, NY, USA (1994) 14. Shepherdson, J.: Negation as failure, completion and stratification. In: in Handbook of Logic in Artificial Intelligence and Logic Programming. Volume 5. Oxford Science Publications (1998) 15. van Zee, M.: Implementing Temporal Action Logics. Master’s thesis, Utrecht University (2013)