Linköping Studies in Science and Technology
Thesis No. 1329

Deductive Planning and Composite
Actions in Temporal Action Logic
by

Martin Magnusson

Submitted to Linköping Institute of Technology at Linköping University in partial
fulfilment of the requirements for degree of Licentiate of Engineering
Department of Computer and Information Science
Linköpings universitet
SE-581 83 Linköping, Sweden

Linköping 2007

Deductive Planning and Composite Actions in
Temporal Action Logic
by
Martin Magnusson
September 2007
ISBN 978–91–85895–93–9
Linköping Studies in Science and Technology
Thesis No. 1329
ISSN 0280–7971
LiU–Tek–Lic–2007:38
ABSTRACT
Temporal Action Logic is a well established logical formalism for reasoning about action andchange that has long been used as a formal specification language. Its first-order characterization and explicit time representation makes it a suitable target for automated theorem
proving and the application of temporal constraint solvers. We introduce a translation froma subset of Temporal Action Logic to constraint logic programs that takes advantage of thesecharacteristics to make the logic applicable, not just as a formal specification language, but insolving practical reasoning problems. Extensions are introduced that enable the generationof action sequences, thus paving the road for interesting applications in deductive planning.
The use of qualitative temporal constraints makes it possible to follow a least commitment
strategy and construct partially ordered plans. Furthermore, the logical language and logic
program translation is extended with the notion of composite actions that can be used toformulate and execute scripted plans with conditional actions, non-deterministic choices, andloops. The resulting planner and reasoner is integrated with a graphical user interface in ourautonomous helicopter research system and applied to logistics problems. Solution plans
are synthesized together with monitoring constraints that trigger the generation of recovery
actions in cases of execution failures.
This work is supported in part by a grant from the Swedish national aeronautics research
program NFFP04 S4203 and a Swedish research council grant 50364201.

Department of Computer and Information Science
Linköpings universitet
SE-581 83 Linköping, Sweden

Acknowledgments
I would like to thank my advisor Patrick Doherty for his contagious enthusiasm
for research, for entrusting me with great freedom in pursuing whatever topics
that have interested me, and for paying me to enjoy my hobby. Two othergreat researchers that I have had the pleasure of collaborating with are Jonas
Kvarnström and Andrzej Szalas. I am looking forward to more opportunities
for joint work in the future.
My colleges at the department of Computer Science at Linköping University
has made it a wonderful environment to work in. I sincerely thank Per Nyblom,
David Landén, Gustav Nordh, Per-Olof Petersson, Fredrik Heintz, and Tommy
Persson for being such good friends. Thank you Jenny Ljung, Anna Maria
Uhlin, Madeleine Häger Dahlqvist, and Piotr Rudol for invaluable assistance.
The choice to pursue academic studies was made with the encouragement
and support from Eva-Lena Lengquist with whom I have had the great fortune
to share many happy moments. Steve Pavlina has unknowingly helped metremendously towards my goal through his innumerable inspirational writings
on how to improve any and every area of your life. My final note of gratitude
goes to my parents and sister for your unconditional love.

Contents
1 Introduction
1.1 The Case for Deductive Planning . . . . . . . . . . . . . . . . .
1.2 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.3 Publications . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.4 Thesis Outline . . . . . . . . . . . . . . . . . . . . . . . . . . .

1
2
2
4
4

2 Temporal Action Logic
2.1 Basic Concepts . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.2 A TAL Narrative . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3 The High-level Language . . . . . . . . . . . . . . . . . . . . . .
2.3.1 The Translation Function . . . . . . . . . . . . . . . . .
2.4 Foundational Axioms . . . . . . . . . . . . . . . . . . . . . . . .
2.5 Circumscription Policy . . . . . . . . . . . . . . . . . . . . . . .
2.6 Reasoning in TAL . . . . . . . . . . . . . . . . . . . . . . . . .
2.6.1 Natural Deduction . . . . . . . . . . . . . . . . . . . . .
2.6.2 Automated Reasoning . . . . . . . . . . . . . . . . . . .

5
5
6
7
8
10
11
12
12
14

3 Deductive Planning
3.1 Reified Action Occurrences . . . . . . . . . . . . . . . . . . . .
3.2 Interval Occlusion . . . . . . . . . . . . . . . . . . . . . . . . .
3.2.1 Temporal Constraint Formalisms . . . . . . . . . . . . .
3.3 A Constructive Plan Existence Proof . . . . . . . . . . . . . . .

15
15
17
18
19

4 Compiling TAL into Logic Programs
4.1 L(ND) Narrative . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2 Translation from L(ND) to L(FL) . . . . . . . . . . . . . . . .
4.3 Introducing Interval Occlusion . . . . . . . . . . . . . . . . . .
4.4 Transformation to Horn Form . . . . . . . . . . . . . . . . . . .
4.5 Circumscription Policy . . . . . . . . . . . . . . . . . . . . . . .

27
28
29
30
32
34

vii

viii

CONTENTS

4.6
4.7

Clauses and Rules . . . . . . . . . . . . . . . . . . . . . . . . .
Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

35
41

5 Composite Actions
5.1 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . .
5.2 Fixpoint Expansion . . . . . . . . . . . . . . . . . . . . . . . . .
5.2.1 Expansion Example . . . . . . . . . . . . . . . . . . . .
5.3 Compiling Composite Actions . . . . . . . . . . . . . . . . . . .
5.3.1 The Compilation Function . . . . . . . . . . . . . . . . .
5.3.2 An Example Composite Action . . . . . . . . . . . . . .
5.4 Reified Composite Actions . . . . . . . . . . . . . . . . . . . . .

45
45
46
46
49
49
51
52

6 A UAV Logistics Application
6.1 Graphical User Interface . . . . . . . . . . . . . . . . . . . . . .
6.2 Execution and Monitoring . . . . . . . . . . . . . . . . . . . . .

53
54
56

7 Related Work59

8 Discussion
8.1 Future Research . . . . . . . . . . . . . . . . . . . . . . . . . .
8.2 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

65
66
67

A The Logistics Scenario Prolog Code69

B Proofs
B.1 Interval Persistence Formula . . . . . . . . . . . . . . . . . . . .
B.2 Interval End-point Equivalence . . . . . . . . . . . . . . . . . .
B.3 Point-interval Rewrite . . . . . . . . . . . . . . . . . . . . . . .
B.4 Shared Timepoint Overlap Equivalence . . . . . . . . . . . . . .

75
75
76
78
80

Chapter 1

Introduction
Artificial intelligence is the challenge of creating a thinking machine. Althoughdefinitions of intelligence and thinking are plentiful, some capabilities seem
absolutely necessary for any system proposed as either. Of central importanceis the capability for rational reasoning, especially reasoning about what canbe done to achieve ones goals. Work within the methodology of formal logic
provides a comprehensive toolset for correct reasoning and is thus a natural
choice for progress toward this end. However, the standard philosophical logic
turns out to be inadequate, and artificial intelligence researchers are therefore
creating new powerful logics that are applicable to human-like commonsense
reasoning as well as more traditional logical reasoning.
Temporal Action Logic (TAL) [8] is one such logic developed at Linköping
University. TAL has, since its inception more than ten years ago, proven to be ahighly versatile and expressive formalism. Nevertheless, many important areasof research can be identified that provide excellent opportunities for improving
the logic. In this thesis we present extensions to TAL that make it applicable
to deductive planning, i.e. reasoning about what actions achieve a given goal,
and we touch upon the topic of composite actions, i.e. complex actions built
from simpler actions, conditionals and loops.
This and most other artificial intelligence research pursued at Linköping
University is part of the Autonomous Unmanned Aerial Vehicle (UAV) Technologies Laboratory and its long-term basic research initiative [6] that focuseson the development of autonomous robots that display high-level cognitive behaviour with the primary experimental platforms being autonomous UAVs.
Having such working systems in mind helps put emphasis on techniques that1

2

Introduction

are not purely of theoretical interest but also useful in practice. We want tomake logic work.

1.1

The Case for Deductive Planning

By deductive planning we shall understand the direct synthesis of plans througha deductive proof process in a logic of action and change. In contrast most of
the work in automated planning makes use of algorithms, formalisms, andprograms specialized for the planning task. This kind of automated planning
has seen great progress and has developed into a well-defined research topic
with specialized conferences and a respectable body of work. In light of thisfact, one might question the need to cast the planning process as deduction.
To answer this question we would like to appeal to the bigger picture. The
artificial intelligence challenge requires an attempt at building a generally intelligent system that is applicable to all problems of any complexity. To bepractically possible this would seem to require formalisms and technologies thatexhibit two important properties. First, note that it is clearly impossible toforesee all possible problems requiring intelligence, in advance of the artificial
agent being confronted by them, and to develop special purpose solutions toeach and every one of them. The alternative is a striving for a property of
uniformity that would allow most problems to be expressed in a similar way,
and different or unforeseen problems to be attacked using the same techniques.
This necessitates the second property of expressivity, to have the ability to encode all the different complexities of problems, and to be able to reason withthem in the same framework. Deductive planning contributes uniformity since
the planning process is cast as deduction in the same way as other types ofreasoning such as prediction. It also supports expressivity since the logics used
are often among the most expressive formalisms known that can be used to
encode complex problems in a well understood way.
Before we get too carried away, however, let us admit that the present stateof deductive planning still has a long way to go before fulfilling these ideals.
The point we would like to make is that work in this direction is important andthat deductive planning enjoys properties that could help progress towards thelong term (as well as the short term) goal.

1.2

Contributions

One of the distinguishing characteristics of Temporal Action Logic is its useof explicit time structures whose meaning can be explained through seman-1.2. Contributions

3

tic attachment or through axiomatizations in classical logic. This feature canbe taken advantage of by combining automated theorem proving with specialized temporal constraint propagation algorithms for dealing with temporal
structures in TAL narratives. First-order automated theorem provers can beinefficient and difficult to use in practical applications, but logic programming,
exemplified by Prolog, is a well-known alternative that has been successfully
applied to many logical reasoning problems. Although logic programming technologies are based on theorem proving, they sacrifice some of the expressivenessof first-order logic to gain simplicity of use and, often, efficiency.
We present a translation from a subset of the full TAL formalism to logic
programs that use Prolog’s finite domain constraint solver and the Constraint
Handling Rules [10] framework. The resulting programs take advantage of these
constraint solving tools to make TAL directly applicable to practical planningproblems in our autonomous Unmanned Aerial Vehicle (UAV) system. TAL
has been used in previous work as a formal specification language for a very
powerful forward-chaining planner called TALplanner [7]. A formally specified
TAL goal narrative is input into the procedural planner, which in turn outputs aplan narrative whose formal semantics is also based on TAL. In this case, TAL is
used as a formal specification tool and the plan generation mechanism operates
outside the logic. In contrast, this thesis introduces additional extensions to
TAL that enable deductive planning at the object level rather than metatheoretically. In order to do this both action occurrences and sets of action
occurrences (a form of plan or narrative) will be introduced as terms and setsin the object language, respectively. In this manner, one may generate partiallyordered plans deductively through the execution of the constraint logic programthat was translated from the TAL narrative.
Since the reasoning is deductive, the process works both ways. One may
provide a complete plan as input and deduce its effects, specify only declarative goals that need to be satisfied, or explore the middle ground between
these extremes. Sometimes, though, one may want to provide a complete planfor the robot to execute that can not be expressed as a sequence of simple actions. Many tasks involve choices that are conditional on some property of theworld, or the repeated application of some sequence of actions until a condition
has been satisfied. We extend the TAL language with macros that enable theencoding of such composite actions and extend the constraint logic programming translation so that they can be executed in the same logic programming
framework.
This framework, named PARADOCS for Planning And Reasoning As DeductiOn with ConstraintS, has been integrated with our UAV system and applied to a logistics scenario. A UAV operator can set up a mission graphically4Introduction

through a user interface, which also visualizes the resulting plan and its execution. Value persistency constraints in the plan are continually monitored, andtrigger failure recovery when violated. Recovery is possible by providing theplan fragment that has yet to be executed as input to the deductive plannerand reasoner. It will complete the partial plan with additional recovery actions
as needed to make it valid again.

1.3

Publications

Parts of this thesis have previously been presented in the following publications:
[24]

[25]

1.4

Martin Magnusson and Patrick Doherty. Deductive planning withtemporal constraints using TAL. In Proceedings of the International Symposium on Practical Cognitive Agents and Robots(PCAR’06), 2006.
Martin Magnusson and Patrick Doherty. Deductive planning withtemporal constraints. In Logical Formalizations of Commonsense
Reasoning: Papers from 2007 AAAI Spring Symposium, Technical
Report SS-07-05, 2007.

Thesis Outline

The structure of this thesis is as follows. Chapter 2 provides an introduction to
Temporal Action Logic sufficient to support understanding of the subsequent
chapters. Chapter 3 introduces extensions that enable deductive planning withTAL and provides an example constructive proof of a simple planning goalfrom which a solution plan can be extracted. Chapter 4 details the compilation
process that automates the planning process using constraint logic programming and temporal constraint formalisms. Chapter 5 specifies the semantics
of composite actions and complements the compilation process so that they
can be evaluated. Chapter 6 presents an integration of the developed methods
with the UAV platform and demonstrates the application of the system to alogistics problem. Chapter 7 relates the work to some of its sources of inspiration. Chapter 8 sums up the results and discusses future directions of research.
Finally, an appendix contains the Prolog clauses that were used in the logistics
application.

Chapter 2

Temporal Action Logic
Temporal Action Logic has its roots in Sandewall’s book Features and Fluents[32] published in 1994 but has since then been developed in a direction of
its own by Doherty, Karlsson, Gustafsson, Kvarnström, and others (see e.g.
[5, 17, 12, 19]). TAL differs from the well-known Situation Calculus and otherlogical formalisms for reasoning about action and change with its use of explicit
time, occlusion, and a high-level language that provides an abstraction layer
free from technical constructions introduced to deal with the frame and otherproblems.
This introduction to TAL is meant to be self contained, but by no means
a complete feature list. A more detailed presentation of TAL is available elsewhere [8].

2.1Basic Concepts

Most logics have an ontological base in properties and relations between objects.
In TAL, properties and relations are modelled using fluents that assume values.
Fluents are typed, so a given fluent only accepts arguments and only takes onvalues from the pre-specified domains. E.g., the location of a robot could bemodelled using a boolean fluent loc(robot,location) that is associated with thevalue true or false for robot and location arguments from the domains robot
and location. Alternatively one could use a location-valued fluent loc(robot)
that has as value the object representing the location of the robot.
Fluents could be written as predicates in first-order logic. However, predicates can not have any values other than true or false and never change theirvalues. In contrast, the value of the loc fluent can be a location that may change
56Temporal Action Logic

over time as the robot moves around. One could get around this problem byintroducing a timepoint and a value argument to the predicate. However, byrepresenting fluents as terms instead of predicates one also gains the possibility of quantifying over them. A special predicate Holds(timepoint,fluent,value)
is introduced to associate a value with a fluent term at a specific timepoint.
Timepoints are explicit objects in the form of numbers or terms that refer toa time-line consisting of positive integers starting with zero.
Suppose we are interested in robotic UAVs and would like to model theirability to move to new locations. The effects of an action fly(uav,location)
would be formally specified and that specification could later be used to reason
about the consequences of occurrences of this action at specific timepoints. An
Occurs(timepoint,timepoint,action) predicate is used for these purposes andrepresents an action occuring over the time interval between two timepoints.
Finally, the concept of occlusion is introduced as a very flexible solution
to the frame and related problems. The basic idea is to make fluent values
persist over time by minimizing their opportunities for change. A predicate
Occlude(timepoint,fluent) represents the possibility of a fluent to change its
value. Negated occlusion is then the property of a fluent retaining its value
from the previous timepoint, axiomatized as:∀t [¬Occlude(t + 1, f ) → ∀v [Holds(t, f, v) ↔ Holds(t + 1, f, v)]]

(1)

Formulas that model a reasoning domain must be written so that fluents are
explicitly occluded in situations where they are known to change values, suchas in the effects of an action. Instead of adding additional negated occlusion
formulas one would like to minimize the number of timepoints where fluentsare occluded to implement the default assumption that things do not change
without a reason. This minimization is effected through circumscription of the
Occlude predicate with respect to parts of the theory as detailed in Section 2.5.
The result is a solution to the frame problem with fine grained control overwhich fluents are persistent at which timepoints.

2.2

A TAL Narrative

The TAL language thus includes three predicates, Holds, Occurs, and Occlude
in an order-sorted (i.e. supporting a type hierarchy) first-order logic. An encoding of a limited domain of knowledge is called a TAL narrative. Consider avery simple reasoning domain involving the flight of a UAV to a new location,
expressed by the following narrative:

2.3. The High-level Language

Holds(0, loc(uav1), loc1)
Occurs(3, 8, fly(uav1, loc2))∀t1 , t2 , u, l [t1 < t2 ∧ Occurs(t1 , t2 , fly(u, l)) →Holds(t2 , loc(u), l) ∧ ∀t [t1 < t ≤ t2 → Occlude(t, loc(u))]]∀t, u [¬Occlude(t + 1, loc(u)) →∀v [Holds(t, loc(u), v) ↔ Holds(t + 1, loc(u), v)]]

7

(2)
(3)
(4)
(5)

Formulas (2) and (3) state that uav1 is located at loc1 and then flies to loc2
between timepoints 3 and 8. The action specification formula (4) occludes thelocation fluent from persistence during the flight and makes sure it assumes thecorrect value at the final timepoint of the occurrence interval. Finally, formula(5) instantiates the general persistence formula (1) for the loc fluent.

2.3

The High-level Language

The reification of fluents as terms enable the application of regular first-orderlogic to the problem of reasoning about actions and change over time. But
formulas in the resulting theory must necessarily contain predicates and supporting axioms of a technical nature that are not present in any natural language description of the problem domain that one is trying to formalize. TAL
provides a high-level narrative description language that helps circumvent thisproblem through a clear and concise syntax that lifts the abstraction level up
above technical details. To differentiate this language from the base logic they
are denoted L(ND) (for Language of Narrative Descriptions) and L(FL) (forLanguage of First-order Logic) respectively. The high-level language L(ND)
does not have a proof theory but is seen as a macro language that can be compiled into L(FL) through a translation function Trans. Reasoning can thenproceed using first-order proof techniques as described in Section 2.6.
Consider the same UAV flight domain introduced above but expressed as anarrative in the high-level language L(ND):[0] loc(uav1) =ˆ loc1[3, 8] fly(uav1, loc2)[t1 , t2 ] fly(u, l)R((t1 , t2 ] loc(u) =ˆ l)∀t, u [Per (t, loc(u))]

(6)
(7)
(8)
(9)

Notice how fluents are associated with values using =,ˆ as in the observation
formula (6), and how temporal contexts are indicated simply by preceding
formulas with timepoint or interval indications, as in the action occurrence(7). Formula (8) denotes throughand the reassignment macro R that the8Temporal Action Logic

fly action will cause the location of the UAV to be released from persistence
during flight and settle on the destination when the flight is completed. The
release from persistence is effected through occlusion of the loc fluent, denotedby X((t1 , t2 ] loc(u) =ˆ l), but the domain modeller need not be concerned aboutocclusion since this mechanism is built into the reassignment macro. Finally,
formula (9) will make the location fluent loc persistent by default using themacro Per.
In addition to the type of formulas illustrated above, a narrative may also
include domain and dependency constraints that express conditions that always
hold or dependencies that change the values of fluents when triggered by otherfluent value changes rather than by an explicit action occurrence. These are
powerful features, although we will not make further use of them in this thesis.

2.3.1

The Translation Function

In its full generality, the syntax of L(ND) and its translation into L(FL) is
given by the translation function Trans. The three L(FL) predicates have acorresponding L(ND) syntax given by:def

Trans([t] f =ˆ v) = Holds(t, f, v)
def

Trans([t1 , t2 ] a) = Occurs(t1 , t2 , a)defTrans(X([t] f =ˆ v)) = Occlude(t, f )Action specifications translate into implications with the occurrence of theaction during a non-unit time interval as the antecedent and the (possibly
conditional and non-deterministic) effects in the conclusion:
Trans([t1 , t2 ] a(x)defΦ) = ∀t1 , t2 , x [t1 < t2 ∧Occurs(t1 , t2 , a(x)) → Trans(Φ)]

The value of a fluent that is occluded at a timepoint is unknown without
the presence of additional information. Persistent fluents are associated withpersistency formulas, such as (5), that bind the fluent’s value to the value atthe previous timepoint when not occluded. A durational fluent, on the other
hand, resumes a default value when not occluded. An example could be a fluent
noise that is true while some loud action is being executed but reverts to false
otherwise. Fluents are specified as persistent or durational using the Per and
Dur macros:defTrans(Per (t, f )) = ¬Occlude(t + 1, f ) →∀v [Holds(t, f, v) ↔ Holds(t + 1, f, v)]
def
Trans(Dur (t, f, v)) = ¬Occlude(t, f ) → Holds(t, f, v)

2.3. The High-level Language

9

The reassignment operator R and interval reassignment operator I ensure boththat the fluent assumes the new value and that it is released from any persistence assumptions using the occlusion operator X :defTrans(R((t1 , t2 ] Φ)) = Trans(X((t1 , t2 ] Φ)) ∧Trans([t2 ] Φ)
defTrans(R([t] Φ)) = Trans(X([t] Φ)) ∧Trans([t] Φ)
defTrans(I((t1 , t2 ] Φ)) = Trans(X((t1 , t2 ] Φ)) ∧Trans((t1 , t2 ] Φ)
defTrans(I([t] Φ)) = Trans(X([t] Φ)) ∧Trans([t] Φ)Temporal intervals can be open or closed in either end, may be infinite, andcan occur inside the occlusion operator X. Their translations are illustrated bysome representative examples:defTrans([t1 , ∞) Φ) = ∀t [t1 ≤ t → Trans([t] Φ)]
defTrans((t1 , ∞) Φ) = ∀t [t1 < t → Trans([t] Φ)]
defTrans([t1 , t2 ] Φ) = ∀t [t1 ≤ t ≤ t2 → Trans([t] Φ)]
defTrans(X((t1 , t2 ] Φ)) = ∀t [t1 < t ≤ t2 → Trans(X([t] Φ))]The translation function ignores connectives and quantifiers, and temporal contexts are distributed over connectives:def

Trans(¬Φ) = ¬Trans(Φ)
defTrans(Φ C Ψ) = Trans(Φ) C Trans(Ψ) where C ∈ {∧, ∨, →, ↔}defTrans(Qv[Φ]) = Qv[Trans(Φ)] where Q ∈ {∀, ∃}def

Trans([t] ¬Φ) = ¬Trans([t] Φ)
defTrans([t] Φ C Ψ) = Trans([t] Φ) C Trans([t] Ψ) where C ∈ {∧, ∨, →, ↔}defTrans([t] Qv[Φ]) = Qv[Trans([t] Φ)] where Q ∈ {∀, ∃}However, the occlusion operator X needs special attention. For the circumscription of Occlude to be computable, as described in Section 2.6, all thefluents that might be influenced by an action must be occluded. This is accomplished by removing negations and replacing disjunctions and existential
quantifiers by conjunctions and universal quantifiers:
def

Trans(X([t] ¬Φ)) = Trans(X([t] Φ))
defTrans(X([t] Φ C Ψ)) = Trans([t] Φ) ∧Trans([t] Ψ) where C ∈ {∧, ∨, →, ↔}defTrans(X([t] Qv[Φ])) = ∀v [Trans(X([t] Φ))] where Q ∈ {∀, ∃}10

Temporal Action Logic

Finally, some common expressions have shorthand notation. If f is a boolean
fluent then f and ¬f are short for f =ˆ true and f =ˆ false, and when several
timepoints are ordered in a series t1 < t2 < t3 , it is short for a conjunctiont 1 < t2 ∧ t 2 < t3 .

2.4Foundational Axioms

Some intuitions about narratives need to be expressed as additional axioms
before the domain of interest can be considered formalized. Specifically, theseinclude unique names assumptions, unique value assumptions, and the meaningof functions and relations on timepoints.
When two different objects, such as loc1 and loc2, are used one most probably assumes that they are different, i.e. that the terms satisfy loc1 6= loc2.
These assumptions have to be made explicit in first-order logic using additional
unique names axioms. Since the logic is order-sorted one may still assume thattwo objects of different types are not the same object, but for any pair of object
terms o and o0 of the same domain the following axiom is added:o 6= o0
The same assumption of uniqueness holds for fluents although two sets of formulas are needed. One with each pair of different fluents f and f 0 , and one
where, for each fluent, one or more of its arguments are different:∀x, y [f (x) 6= f 0 (y)]∀x1 , . . . , xn , y1 , . . . , yn [x1 6= y1 ∨ · · · ∨ xn 6= yn →f (x1 , . . . , xn ) 6= f (y1 , . . . , yn )]Similar unique names axioms are added for action terms:∀x, y [a(x) 6= a0 (y)]∀x1 , . . . , xn , y1 , . . . , yn [x1 6= y1 ∨ · · · ∨ xn 6= yn →a(x1 , . . . , xn ) 6= a(y1 , . . . , yn )]Unique value axioms, two for each fluent, state that the fluent holds one, andexactly one, value at each timepoint:∀t, x [∃v [Holds(t, f (x), v)]]∀t, x, v1 , v2 [v1 6= v2 → ¬(Holds(t, f (x), v1 ) ∧ Holds(t, f (x), v2 ))]2.5. Circumscription Policy

11

Finally, some of the formulas we have used include the addition function + andthe “less than” relation < and “less than or equal” relation ≤ on integer timepoints. The intention is for them to behave like the mathematical concepts withcorresponding notation. It is possible to include an axiomatized theory for thispurpose, such as Presburger arithmetic [39], and continue using regular theorem proving with the additional axioms. However, from a practical viewpoint,a more realistic approach is the use of a specialized but incomplete reasoning
system, e.g. some variant of a constraint solver as discussed in Section 3.2.1
and carried out in Chapter 4.

2.5

Circumscription Policy

Value changes of fluents that have been specified as persistent are minimized
through circumscription, in effect implementing a default assumption of persistence unless an exception was explicitly stated using the Occlude predicate. A
circumscription policy specifies what predicates to minimize in which formulas,
thereby making sure the expected behaviour is obtained. To specify the policy
we need to be able to refer to the different sets of formulas that a narrative
consists of. For this purpose, let Γfnd denote the foundational axioms, Γperpersistence formulas, Γobs fluent value observations, Γdomc domain constraints,
Γocc action occurrences, Γdepc dependency constraints, and Γacs denote action
specifications. The TAL circumscription policy is then given by:Γfnd ∧ Γper ∧ Γobs ∧ Γdomc ∧ CIRC [Γocc ; Occurs] ∧ CIRC [Γdepc ∧ Γacs ; Occlude]
The Occurs predicate is minimized to remove the possibility of unknown action
occurrences. Since action effects entail occlusion they would otherwise prevent
proofs of persistence. Note also that persistence formulas (Γper ) are excluded
from the minimization of Occlude even though they contain the predicate. The
contrapositive of the persistence formula (1) illustrates the reason:∀t [¬∀v [Holds(t, f, v) ↔ Holds(t + 1, f, v)] → Occlude(t + 1, f )](10)

If (1), which is equivalent to (10), had been included, a fluent value change
would have been reason in itself for the occlusion of a fluent, and the minimization of Occlude would not have been effective.

12

2.6

Temporal Action Logic

Reasoning in TAL

The goal of the development of Temporal Action Logic is not just to formalize
reasoning domains, but also to make it possible for an intelligent agent to use
the logic to perform practical reasoning tasks. The availability of reasoning
techniques is therefore of great importance, and it is no coincidence that firstorder logic was chosen for the base language. Nevertheless, after narratives
written in the high-level language L(ND) have been compiled into the firstorder language L(FL), the circumscription policy is applied and the resulting
theory is second-order, where no complete proof methods are possible. By enforcing certain syntactic restrictions on the L(ND) formulas one can show thatthe circumscribed predicates Occurs and Occlude occur only positively in therelevant parts of the theory, Γocc and Γdepc ∧Γacs respectively [8]. Circumscription then reduces to predicate completion [22], which can be computed withrelative ease. Any first-order proof method of choice can then be applied.

2.6.1

Natural Deduction

A natural deduction proof of a simple consequence of the UAV narrative introduced in Section 2.2 will serve to illustrate reasoning in TAL. The notation
used is that of Copi [31], where each row is made up of a row number (startingfrom 11 to avoid confusing the row numbers with numbered formulas in previous sections of this chapter), the deduced formula, and a justification of thededuction. We will not explicitly list the natural deduction rules used in thejustification but instead assume proof steps that are sufficiently small so as toonly require justification in the form of references to the proof rows that the
deduction depends on, or a letter indicating a premise P , hypothesis H, tautology T , or a direct consequence of the TAL foundational axioms F . The scopeand nesting of hypotheses are indicated by vertical lines in the left margin.
Assume that we would like to prove e.g. that uav1 will be at loc2 at timepoint 9. The proof begins by predicate completion of Occurs in the action
occurrence formula subset Γocc of the narrative (simply formula (3) above) andof Occlude in the action specification and dependency constraint formula subset Γdepc ∧ Γacs of the narrative (simply formula (4) above), according to thecircumscription policy. The resulting premises are:
11 Holds(0, loc(uav1), loc1)
12 ∀t1 , t2 , a [t1 = 3 ∧ t2 = 8 ∧ a = fly(uav1, loc2) ↔ Occurs(t1 , t2 , a)]PP

13 ∀t1 , t2 , u, l [t1 < t2 ∧ Occurs(t1 , t2 , fly(u, l)) → Holds(t2 , loc(u), l)]P
14 ∀t, u [∃t1 , t2 , l [t1 < t ≤ t2 ∧ Occurs(t1 , t2 , fly(u, l))] ↔ Occlude(t, loc(u))] P

2.6. Reasoning in TAL

13

15 ∀t, u [¬Occlude(t + 1, loc(u)) →∀v [Holds(t, loc(u), v) ↔ Holds(t + 1, loc(u), v)]]

P

Note that the action specification formula gave rise to both an action effectformula and the occlusion definition in premises (13) and (14), and that thefoundational axioms are not present in this listing.
We proceed to show that the fly action takes the UAV to loc2 between
timepoints 3 and 8:
16 3 < 8 ∧ Occurs(3, 8, fly(uav1, loc2)) → Holds(8, loc(uav1), loc2)
17 3 < 813F

18 3 = 3 ∧ 8 = 8 ∧ fly(uav1, loc2) = fly(uav1, loc2) ↔
Occurs(3, 8, fly(uav1, loc2))
19 3 = 3 ∧ 8 = 8 ∧ fly(uav1, loc2) = fly(uav1, loc2)

1220 Occurs(3, 8, fly(uav1, loc2))
21 Holds(8, loc(uav1), loc2)

T18, 1916, 17, 20

The minimization of Occlude has made it possible to prove non-occlusion of
the loc fluent for timepoints outside the fly action occurrence interval. Thisfact, together with the persistence formula (15), is required to propagate thefluent’s value loc2 from timepoint 8 to timepoint 9:
22 ¬Occlude(8 + 1, loc(uav1)) →Holds(8, loc(uav1), loc2) ↔ Holds(8 + 1, loc(uav1), loc2)
23 8 + 1 = 9
24 ¬Occlude(9, loc(uav1)) →Holds(8, loc(uav1), loc2) ↔ Holds(9, loc(uav1), loc2)
25 ¬∃t1 , t2 , l [t1 < 9 ≤ t2 ∧ Occurs(t1 , t2 , fly(uav1, l))] ↔
¬Occlude(9, loc(uav1))∃t1 , t2 , l [t1 < 9 ≤ t2 ∧ Occurs(t1 , t2 , fly(uav1, l))]26

15
F22, 2314
H

27

t1 < 9 ≤ t2 ∧ Occurs(t1 , t2 , fly(uav1, l))28

t1 = 3 ∧ t2 = 8 ∧ fly(uav1, l) = fly(uav1, loc2)

12, 27

29
30

3<9≤8
false

27, 28
29, F

31

false

32 ¬∃t1 , t2 , l [t1 < 9 ≤ t2 ∧ Occurs(t1 , t2 , fly(uav1, l))]33 ¬Occlude(9, loc(uav1))

H

26, 27 − 30
26 − 3125, 32

14

Temporal Action Logic

34 Holds(8, loc(uav1), loc2) ↔ Holds(9, loc(uav1), loc2)
35 Holds(9, loc(uav1), loc2)

2.6.2

24, 3321, 34

Automated Reasoning

Beside handcrafted proofs, a whole host of automated theorem proving andmodel theoretic tools are in principle applicable to the first-order narrative.
Unfortunately it is far from self-evident that the direct application of theorem
provers provides reasoning capabilities that are sufficiently efficient to be ofpractical use. Especially not when an axiomatization of TAL’s integer time
structure is used.
In practice we most often rely on a model theoretic tool for evaluating TAL
formulas and visualizing their models developed by Kvarnström called VITAL[18]. The tool, which is available online, provides excellent opportunities forexperimentation with formalizing reasoning problems as TAL narratives.
This thesis explores a third option, the use of logic programming and constraint solving technology. By introducing further restrictions on L(ND) formulas it is possible to define a compilation into logic programs that can be efficiently executed by Prolog. Furthermore, the close integration between Prolog
and constraint solvers, in the constraint logic programming paradigm, provides
a good fit to the TAL logic with its explicit time structures. This topic is
explored in Chapter 4 and Chapter 5.

Chapter 3

Deductive Planning
Deductive planning requires modifications to the Temporal Action Logic presented in Chapter 2. When action occurrences are specified using the first-order
predicate Occurs there is no mechanism that allows the addition of new occurrences through a deductive proof process. Hypothesizing new instances of thispredicate given a goal would require abductive techniques or the use of somespecial-purpose planning algorithm such as that employed by TALplanner [7].
This chapter introduces a deductive mechanism through the reification of action
occurrences as terms in the language that can be reasoned with and quantified
over. In addition, TAL is extended with the concept of interval occlusion thatmakes the use of temporal constraint formalisms easier. Constraint solvers
eliminate the need for an axiomatization of the integer timeline for the typesof temporal reasoning needed in our applications to deductive planning. A
hand crafted proof illustrates how reified actions and interval occlusion makeplanning possible, although still not practical.

3.1

Reified Action Occurrences

A deductive planning goal Φ is usually expressed as the existence of a plan thatsatisfies Φ. In TAL we would add an explicit timepoint at which the goal issatisfied:∃t, p [Φ(t, p)]
While the conclusion in proving the above is the existance of a plan, the actual
plan can be retrieved from that proof. However, since plans are composed ofaction occurrences that are denoted using the TAL predicate Occurs, there is15

16

Deductive Planningno way to specify a (first-order) existential quantifier over plans in TAL. This
problem can be resolved by reifying action occurrences as terms, which can bequantified over. Doing so necessitates the introduction of a Member predicate,to group action occurrence terms into sets, or plans, and the addition of a new
action occurrence set argument to the other two TAL predicates Holds andOcclude, so that we can talk about e.g. a fluent’s value in the context of a
specific plan.
We start by introducing a function occ that replaces action occurrences
Occurs(t1 , t2 , a) by terms of the form occ(t1 , t2 , a). A set of action occurrences
is a set of such terms. The temporal ordering of the actions themselves isgiven by their relations to the explicit time line, determined by the t1 and t2
timepoint arguments. In consequence, the order of the action occurrence terms
in the set is not important, which means that its behaviour is just like a regularmathematical set.
Additionally, a vital property is incompleteness of the action occurrence set.
If a reasoning problem involves a fully specified set of action occurrences, thenthe problem corresponds to prediction or postdiction of the effects of executing the actions or the conditions that hold when executing those actions. If areasoning problem involves an under-specified (or empty) set of action occurrences, then the problem often involves the addition of new action occurrences
to the occurrence set to satisfy goal constraints that were expressed as part ofthe problem. This constitutes a process of deductive planning.
We introduce a composition function term cons(a, p) to add an individual
action occurrence term a to an action occurrence set (or plan) p, and the term
nil to represent the empty set. A predicate Member is associated with a simple
axiomatization of set membership:∀x [¬Member (x, nil )]∀x, y, s [Member (x, cons(y, s)) ↔ x = y ∨ Member (x, s)]
A new Occurs predicate with an additional action occurrence set argument isdefined as:∀t1 , t2 , a, p [Occurs(t1 , t2 , a, p) ↔ Member (occ(t1 , t2 , a), p)]
Lastly, an action occurrence argument is added to the other two L(FL) predicates Holds and Occlude. The meaning of a narrative is preserved by introducing a new universally quantified action occurrence set variable p in each of thenarrative formulas. E.g., the fly action specification formula from the example
narrative in Chapter 2, repeated here:3.2. Interval Occlusion

17∀t1 , t2 , u, l [t1 < t2 ∧ Occurs(t1 , t2 , fly(u, l)) →Holds(t2 , loc(u), l) ∧ ∀t [t1 < t ≤ t2 → Occlude(t, loc(u))]]would receive an additional universally quantified action occurrence set argument p simply by adding it to each of the L(FL) predicates:∀t1 , t2 , u, l, p [t1 < t2 ∧ Occurs(t1 , t2 , fly(u, l), p) →Holds(t2 , loc(u), l, p) ∧ ∀t [t1 < t ≤ t2 → Occlude(t, loc(u), p)]]Using the same variable p throughout the formula ensures that dependencies on
action occurrences are preserved just as if the occurrences had been specified
separately using the old Occurs predicate. Then, by universal quantification
over p, the formula is made applicable for any set of action occurrences that
one might want to reason about.

3.2

Interval Occlusion

The TAL Occlude predicate determines at which timepoints a fluent may
change value. Negated occlusion is, accordingly, the property of a fluent not
being allowed to change, i.e. the property of persistence. Proofs of persistence between two timepoints are very frequent in the context of planningand the most straightforward way of proving persistence involves deducing¬Occlude(ti , f ) for the fluent of interest f and for all intermediate timepoints
ti . A fluent persistency formula is then applied to propagate the fluent’s value
from one timepoint to the other.
However, when the number of intermediate timepoints is not known thesimple proof sketched above is not applicable. This is the case e.g. when only
qualitative timepoints are used, or when a least commitment strategy concerning the timepoints and orderings of action occurrences is strived for. In suchcases it is more useful to look at all the intermediate timepoints as an interval
and persistence over all the timepoints as interval persistence. As a first stepin this direction we introduce the interval occlusion predicate Occlude(t1 , t2 , f )(or Occlude(t1 , t2 , f, p) if action occurrences are reified). The intended meaningis that fluent f is interval occluded over (t1 , t2 ] iff it is occluded at some timepoint in that interval. Conversely, if we manage to prove that fluent f is notinterval occluded for t1 and t2 , then we know that its value will persist. Formally, we define interval occlusion in terms of the regular timepoint occlusionas:∀t1 , t2 , f [Occlude(t1 , t2 , f ) ↔ ∃t [t1 < t ≤ t2 ∧ Occlude(t, f )]](1)

In Appendix B.1 we prove that (1) together with the persistence formula for
timepoint occlusion entails an interval persistence formula:18

Deductive Planning∀t1 , t2 , f [¬Occlude(t1 , t2 , f ) →∀t [t1 < t ≤ t2 → ∀v [Holds(t − 1, f, v) ↔ Holds(t, f, v)]]](2)

Note that even if a fluent is interval occluded over a given interval, it is notnecessarily occluded in all sub-intervals. However, if the fluent is interval persistent over the interval it must also be persistent in all sub-intervals. As shownin Appendix B.2, formulas (1) and (2) entail the following formula:∀t1 , t2 , f [¬Occlude(t1 , t2 , f ) → ∀v [Holds(t1 , f, v) ↔ Holds(t2 , f, v)]]

(3)

Using (3), the truth value of a fluent can be made to “jump” any number of
timepoints in a single proof step. This technique is essential in the translation
to constraint logic programs described in Chapter 4.

3.2.1

Temporal Constraint Formalisms

Another essential step towards efficient proof procedures for TAL in the context
of only qualitative and partial knowledge of temporal relations is the introduction of temporal constraint propagation techniques. While the Holds(t, f, v)
predicate is defined on timepoints, both the Occurs(t1 , t2 , a) and the new
Occlude(t1 , t2 , f ) predicates are defined over intervals characterized by their
end-points t1 and t2 . Furthermore, considering persistence over entire intervals was found to result in conveniently simple persistence proofs. These facts
suggest that the well-known interval algebra formalism introduced by Allen[1], which adopts the interval as a primitive temporal object, might be useful.
Allen shows that thirteen primitive relations exhaust all possible qualitative
relations between two intervals, and the algebra is complete for reasoning withthem, even in the context of incomplete information. Allen also notes thatintervals can be represented by their end-points and primitive relations by ordering conditions on these end-points.
Thornton et. al. [38] go on to show how their end-point ordering model canbe used to express the qualitative interval algebra in a quantitative constraint
solver with finite domains. They recognize that all solutions to an interval
algebra problem must be possible to express by different integer instantiationsof the end-points that satisfy the ordering conditions. Furthermore, if there arem intervals in the problem, 2m is an upper bound on the number of different
integers needed. Hence, an interval algebra network can be encoded as a finite
domain constraint satisfaction problem where variables represent interval endpoints and belong to the range 1 . . . 2m.
We have chosen to work with a finite domain constraint solver and theend-point ordering encoding of the interval algebra, and Chapter 4 provides
details on how this is used to implement temporal relations in TAL narratives

3.3. A Constructive Plan Existence Proof

19

expressed as logic programs. Although, other temporal constraint formalisms
than the interval algebra are certainly possible. We have in fact experimented
with general temporal constraint networks [28], a unifying framework that provides both intervals and timepoints as primitives and both qualitative andquantitative relations between them. Such networks are also associated withcomplete reasoning procedures of the same (exponential) computational complexity. However, the simpler interval algebra end-point ordering model uses
only the <, =, and > relations between timepoints, requiring no extensions ofTAL. General temporal constraint networks support more complex relations
whose description in TAL require some form of semantic attachment. Moreover, the upper bound on the domains of timepoint variables, required whenworking with the finite domain constraint solver, enforces an upper bound on
the number of actions in action occurrence sets. This follows from the fact thateach action occurs over an interval that is added to the interval algebra graph.
Such a bound prevents infinite sequences of actions that can in certain domains
keep the planner busy, preventing it from finding a solution. Completeness canbe achieved through an iterative deepening of this bound. In practice, the finite
domain constraint solver implementation is also considerably faster.

3.3

A Constructive Plan Existence Proof

The above extensions realize planning as deduction. Consider, e.g., the following narrative in L(FL) that extends the narrative in Section 2.2 towards alogistics scenario for UAVs. A location-valued fluent loc(object) and a boolean
fluent carrying(uav,crate) are used to represent the location of an object (either a UAV or a crate) and the fact that a UAV is carrying (or not) a crate
respectively. Two actions, fly(uav,location) and attach(uav,crate), can be used
for flying a UAV to a location and to instruct a UAV to attach its winch toa crate. For the purpose of this example, the narrative formulas make useof interval occlusion. A principled way of introducing interval occlusion in anarrative expressed using regular occlusion is detailed in Section 4.3.
Listing the narrative formulas as premises in the natural deduction style
notation introduced in Section 2.6.1 results in the following rows:
456∀x [¬Member (x, nil )]∀x, y, s [Member (x, cons(y, s)) ↔ x = y ∨ Member (x, s)]∀t1 , t2 , a, p [Occurs(t1 , t2 , a, p) ↔ Member (occ(t1 , t2 , a), p)]

P
P
P

7

∀t1 , t2 , o, p [t1 < t2 ∧ ¬Occlude(t1 , t2 , loc(o), p) →∀v [Holds(t1 , loc(o), v, p) ↔ Holds(t2 , loc(o), v, p)]]P

20

Deductive Planning8∀t1 , t2 , u, c, p [t1 < t2 ∧ ¬Occlude(t1 , t2 , carrying(u, c), p) →∀v [Holds(t1 , carrying(u, c), v, p) ↔ Holds(t2 , carrying(u, c), v, p)]] P

9 ∀t1 , t2 , u, l, p [t1 < t2 ∧ Occurs(t1 , t2 , fly(u, l), p) → Holds(t2 , loc(u), l, p)] P
10 ∀t1 , t2 , u, c, l, p [t1 < t2 ∧ Occurs(t1 , t2 , attach(u, c), p) ∧Holds(t1 , loc(c), l, p) ∧ Holds(t1 , loc(u), l, p) →Holds(t2 , carrying(u, c), true, p) ∧ ¬Holds(t2 , loc(c), l, p)] P
11 ∀t1 , t2 , t3 , t4 , u, c, l, p [t2 > t3 ∧ t1 < t4 ∧ Occurs(t3 , t4 , attach(u, c), p) ∧Holds(t3 , loc(c), l, p) ∧ Holds(t3 , loc(u), l, p) ↔
Occlude(t1 , t2 , carrying(u, c), p)]P
12 ∀t1 , t2 , t3 , t4 , u, c, l, p [t2 > t3 ∧ t1 < t4 ∧ Occurs(t3 , t4 , attach(u, c), p) ∧Holds(t3 , loc(c), l, p) ∧ Holds(t3 , loc(u), l, p) ↔
Occlude(t1 , t2 , loc(c), p)]
P
13 ∀p [Holds(0, loc(uav1), base, p)]
14 ∀p [Holds(0, loc(crate1), loc1, p)]PP

15 ∀u, c, p [Holds(0, carrying(u, c), false, p)]P

Given this narrative one would like to find constructive proofs of plan existence
queries. As an example, it should be possible to prove that there exists someset of action occurrences p (a solution plan) that results in uav1 carrying crate1
at some future timepoint t. The main goal of the proof can then be expressedas the existence of such a timepoint and plan for which the goal holds:∃t, p [Holds(t, carrying(uav1, crate1), true, p)]
The exact value of timepoint t can be unspecified as long as the actions in p
will fit between timepoints 0 and t. A single intermediate timepoint tk suffices
for the purposes of this proof:
16 0 < tk < tPOne way of proving the main goal is by instantiating the attach action specification with uav1, crate1, and t:
17 ∀t1 , l, p [t1 < t ∧ Occurs(t1 , t, attach(uav1, crate1), p) ∧Holds(t1 , loc(crate1), l, p) ∧ Holds(t1 , loc(uav1), l, p) →Holds(t, carrying(uav1, crate1), true, p)]

10

If the implication antecedent of Row 17 can be proven, the goal will follow from
Modus Ponens. Call the four antecedent conjuncts Subgoal 1 – 4. Subgoal 1
can be satisfied immediately:
18 tk < t16

3.3. A Constructive Plan Existence Proof

21

Subgoal 2 requires the use of the definition of Occurs. This creates an action
occurrence set that includes an occurrence of the attach action and a new
unknown plan tail p1 :19 occ(tk , t, attach(uav1, crate1)) = occ(tk , t, attach(uav1, crate1)) ∨Member (occ(tk , t, attach(uav1, crate1)), p1 ) →Member (occ(tk , t, attach(uav1, crate1)),cons(occ(tk , t, attach(uav1, crate1)), p1 ))20 occ(tk , t, attach(uav1, crate1)) = occ(tk , t, attach(uav1, crate1))
21 Member (occ(tk , t, attach(uav1, crate1)),cons(occ(tk , t, attach(uav1, crate1)), p1 ))22 Occurs(tk , t, attach(uav1, crate1),cons(occ(tk , t, attach(uav1, crate1)), p1 ))23 ∀p1 [Occurs(tk , t, attach(uav1, crate1),cons(occ(tk , t, attach(uav1, crate1)), p1 ))]5T19, 206, 21
22

One way of satisfying Subgoal 3, Holds(t1 , loc(crate1), l, p), would be to use
Row 14 that specifies the location of crate1 in the initial state. But t1 would
then be instantiated to 0, which would leave the UAV no time to fly there andsatisfy Subgoal 4. Instead, we use the persistence of the loc fluent to show thatcrate1 remains at loc1 from 0 to an intermediate timepoint tk . An automatedtheorem prover, without foresight, would try both the initial state fact andthe persistence formula, either simultaneously, or through backtracking. The
persistence formula in Row 7 is reformulated as an implication:
24 ∀v, p1 [0 < tk ∧¬Occlude(0, tk , loc(crate1),cons(occ(tk , t, attach(uav1, crate1)), p1 )) ∧Holds(0, loc(crate1), v, cons(occ(tk , t, attach(uav1, crate1)), p1 )) →Holds(tk , loc(crate1), v, cons(occ(tk , t, attach(uav1, crate1)), p1 ))] 7
If the three antecedent conjuncts of Row 24 are referred to as Subgoal 3.1 –
3.3, then Subgoal 3.1 is given by:
25 0 < tk

16

In order to succeed with the proof of non-occlusion in Subgoal 3.2 it is necessary to close the action occurrence argument p1 with respect to any unknown
attach actions. The TAL circumscription policy usually closes action occurrences through circumscription of the Occurs predicate. The same effect canbe achieved with reified action occurrences by recording assumptions madeabout the plan argument p. Such assumptions can be proven after instantiating unbound plan variables to nil when no new occurrences need to be added

22

Deductive Planningto the final plan. The proof of Subgoal 3.2 records the assumption that p1contains no occurrences of attach in Row 26. Non-occlusion of the loc fluent
can be proved using its definition from Row 12. Assuming that the conditions
for occlusion are satisfied, in Row 28, leads to a contradiction. It would either
have meant that the persistence interval (0, tk ] overlaps the attach action interval (tk , t], disproved in Row 29 – Row 34, or that there are some other attach
actions, which we assumed false as shown by Row 35 – Row 37:
26¬∃t1 , t2 , u, c [Member (occ(t1 , t2 , attach(u, c)), p1 )]27¬(tk > t3 ∧ 0 < t4 ∧Occurs(t3 , t4 , attach(u, c), cons(occ(tk , t, attach(uav1, crate1)), p1 )) ∧Holds(t3 , loc(crate1), l, cons(occ(tk , t, attach(uav1, crate1)), p1 )) ∧Holds(t3 , loc(u), l, cons(occ(tk , t, attach(uav1, crate1)), p1 ))) →¬Occlude(0, tk , loc(crate1),cons(occ(tk , t, attach(uav1, crate1)), p1 ))1228

t k > t3 ∧ 0 < t4 ∧Occurs(t3 , t4 , attach(u, c), cons(occ(tk , t, attach(uav1, crate1)), p1 )) ∧Holds(t3 , loc(crate1), l, cons(occ(tk , t, attach(uav1, crate1)), p1 )) ∧Holds(t3 , loc(u), l, cons(occ(tk , t, attach(uav1, crate1)), p1 ))H

29

Member (occ(t3 , t4 , attach(u, c)),cons(occ(tk , t, attach(uav1, crate1)), p1 ))6, 28

occ(t3 , t4 , attach(u, c)) = occ(tk , t, attach(uav1, crate1)) ∨Member (occ(t3 , t4 , attach(u, c)), p1 )

5, 29

31

occ(t3 , t4 , attach(u, c)) = occ(tk , t, attach(uav1, crate1))

H

32
33
34

t3 = tk ∧ t4 = t ∧ u = uav1 ∧ c = crate1
t k > tk ∧ 0 < t⊥

35

Member (occ(t3 , t4 , attach(u, c)), p1 )H

36

∃t1 , t2 , u, c [Member (occ(t1 , t2 , attach(u, c)), p1 )]

35

37

⊥

30

38
39

⊥

H

31
28, 32
33, F

26, 3630, 31 − 34, 35 − 37¬(tk > t3 ∧ 0 < t4 ∧Occurs(t3 , t4 , attach(u, c), cons(occ(tk , t, attach(uav1, crate1)), p1 )) ∧Holds(t3 , loc(crate1), l, cons(occ(tk , t, attach(uav1, crate1)), p1 )) ∧Holds(t3 , loc(u), l, cons(occ(tk , t, attach(uav1, crate1)), p1 ))) 28 − 38

3.3. A Constructive Plan Existence Proof

40

23¬Occlude(0, tk , loc(crate1),cons(occ(tk , t, attach(uav1, crate1)), p1 ))27, 3941 ¬∃t1 , t2 , u, c [Member (occ(t1 , t2 , attach(u, c)), p1 )] →¬Occlude(0, tk , loc(crate1),cons(occ(tk , t, attach(uav1, crate1)), p1 ))26 − 4042 ∀p1 [¬∃t1 , t2 , u, c [Member (occ(t1 , t2 , attach(u, c)), p1 )] →¬Occlude(0, tk , loc(crate1),cons(occ(tk , t, attach(uav1, crate1)), p1 ))]41

Knowledge about the initial state in Row 14 is then used to satisfy Subgoal 3.3
with v instantiated to loc1 :43 ∀p1 [Holds(0, loc(crate1), loc1, cons(occ(tk , t, attach(uav1, crate1)), p1 ))] 14
Subgoal 3 can now be completed, although it is still qualified by the assumption
on occurrences of attach:44¬∃t1 , t2 , u, c [Member (occ(t1 , t2 , attach(u, c)), p1 )]H

45

Holds(tk , loc(crate1), true,cons(occ(tk , t, attach(uav1, crate1)), p1 ))24, 25, 42, 44, 43

46 ∀p1 [¬∃t1 , t2 , u, c [Member (occ(t1 , t2 , attach(u, c)), p1 )] →Holds(tk , loc(crate1), loc1,
cons(occ(tk , t, attach(uav1, crate1)), p1 ))]44 − 45

The fly action specification in Row 9 can be used to prove Subgoal 4. The
definition of Occurs is used to add a fly action to the plan, resulting in a newplan tail p2 . The new action causes the UAV to end up at the location of thecrate, thereby satisfying the last condition for attaching it:
47 0 < tk ∧ Occurs(0, tk , fly(uav1, loc1),cons(occ(tk , t, attach(uav1, crate1)),cons(occ(0, tk , fly(uav1, loc1)), p2 ))) →Holds(tk , loc(uav1), loc1, cons(occ(tk , t, attach(uav1, crate1)),cons(occ(0, tk , fly(uav1, loc1)), p2 )))48 occ(0, tk , fly(uav1, loc1)) = occ(0, tk , fly(uav1, loc1)) ∨Member (occ(0, tk , fly(uav1, loc1)), p2 ) →Member (occ(0, tk , fly(uav1, loc1)), cons(occ(0, tk , fly(uav1, loc1)), p2 ))49 occ(0, tk , fly(uav1, loc1)) = occ(0, tk , fly(uav1, loc1))
50 Member (occ(0, tk , fly(uav1, loc1)),cons(occ(0, tk , fly(uav1, loc1)), p2 ))95
T48, 4924

Deductive Planning51 occ(0, tk , fly(uav1, loc1)) = occ(tk , t, attach(uav1, crate1)) ∨Member (occ(0, tk , fly(uav1, loc1)),cons(occ(0, tk , fly(uav1, loc1)), p2 )) →Member (occ(0, tk , fly(uav1, loc1)),cons(occ(tk , t, attach(uav1, crate1)),cons(occ(0, tk , fly(uav1, loc1)), p2 )))52 Member (occ(0, tk , fly(uav1, loc1)),cons(occ(tk , t, attach(uav1, crate1)),cons(occ(0, tk , fly(uav1, loc1)), p2 )))53 Occurs(0, tk , fly(uav1, loc1),cons(occ(tk , t, attach(uav1, crate1)),cons(occ(0, tk , fly(uav1, loc1)), p2 )))54 Holds(tk , loc(uav1), loc1,
cons(occ(tk , t, attach(uav1, crate1)),cons(occ(0, tk , fly(uav1, loc1)), p2 )))55 ∀p2 [Holds(tk , loc(uav1), loc1,
cons(occ(tk , t, attach(uav1, crate1)),cons(occ(0, tk , fly(uav1, loc1)), p2 )))]

5

50, 51

6, 52

25, 47, 53

54

At this point, Subgoal 1 – 4 in the antecedent of Row 17 have been proved forthe following instantiations of the universally quantified variables:
t1 = tkl = loc1
p1 = cons(occ(0, tk , fly(uav1, loc1)), p2 )p = cons(occ(tk , t, attach(uav1, crate1)),cons(occ(0, tk , fly(uav1, loc1)), p2 ))The qualification on Subgoal 3 can be satisfied by choosing a plan tail p2 that
does not contain any attach actions. The most obvious choice is p2 = nil :56 ∀x, y, s [¬(x = y) ∧ ¬Member (x, s) → ¬Member (x, cons(y, s))]57 ¬(occ(t1 , t2 , attach(u, c)) = occ(0, tk , fly(uav1, loc1)))
58 ¬Member (occ(t1 , t2 , attach(u, c)), nil )5F459 ∀t1 , t2 , u, c [¬Member (occ(t1 , t2 , attach(u, c)),cons(occ(0, tk , fly(uav1, loc1)), nil ))]56, 57, 58

60 ¬∃t1 , t2 , u, c [Member (occ(t1 , t2 , attach(u, c)),cons(occ(0, tk , fly(uav1, loc1)), nil ))]59

3.3. A Constructive Plan Existence Proof

25

This completes the proof of the main goal:
61 Holds(t, carrying(uav1, crate1), true,cons(occ(tk , t, attach(uav1, crate1)),cons(occ(0, tk , fly(uav1, loc1)), nil )))62 ∃t, p [Holds(t, carrying(uav1, crate1), true, p)]17, 18, 23, 46, 55, 60
61

By extracting the plan from the action occurrence set one can utilize deductive
proofs for planning. The above proof was one of many possible constructive
proofs of the goal. Through the application of an automated theorem proverthat considers all the possibilities in the different choice points in the proof
process one obtains a complete planner. However, even the trivial planningproblem solved above had a relatively long and complicated proof. Direct
application of automated theorem provers to an L(FL) narrative would not
result in a practical planning system. Clearly, more work needs to be done
before deductive planning becomes truly useful in practice. This is the topic
of the next chapter.

26

Deductive PlanningChapter 4

Compiling TAL into Logic
Programs
We introduce a four step translation from L(ND) narratives into constraint logic
programs that makes use of the reified action occurrences, interval occlusion,and temporal constraint formalisms described in Chapter 3. The four steps are
as follows:(Section 4.2)
(Section 4.3)
(Section 4.4)
(Section 4.6)

Compile the TAL narrative from the surface language
L(ND) to the first-order logic language L(FL).
Replace timepoint occlusion in formulas by interval occlusion.
Rewrite all formulas into Horn clause form.
Encode the Horn clauses as Prolog clauses, constraint handling rules, and finite domain constraints.

The resulting programs are efficiently evaluated using Prolog and can be used
for both deductive planning and reasoning. The compilation provides a means
for the application of deductive planning in TAL to solving practical reasoning
problems such as those encountered by our UAV research platform.
Any translation to constraint logic programs is bound to be partial since
the source language has the expressivity of first-order logic while the target
language is limited to Horn clause form and the constraint formalisms used.
Restrictions are therefore set up to isolate the class of narratives of interest. To
prevent the implications of this from being lost in the technical details of thetranslation process we conclude this chapter with a summary and discussion in
Section 4.7.
27

28

Compiling TAL into Logic Programs

4.1

L(ND) Narrative

The first restriction is to narratives without domain or dependency constraints.
Such narratives will only consist of action specifications that detail the conditions and effects of actions, persistence statements that specify which fluents
retain their value over time, and observation statements that describe the initialstate of the world. Action specifications are assumed to be of the form:[t1 , t2 ] a(w)∀x [P (y) → E(z)](1)

where y, z ⊆ w ∪ x. P (y) is a conjunction of conditions on fluent values, eachhaving the form:[t1 , t2 ] f (y) =ˆ v
where the end timepoint t2 is optional and the value v could be one of thevariables in w ∪x, or a constant, including the boolean constants true and false.
E(z) is a conjunction of reassignments of fluent values, using the reassignment
macro R, each of the form:
R((t1 , t2 ] f (z) =ˆ v)
ˆ and, again, v belongs to w ∪ x or is a constant.
where =
ˆ can be replaced by 6=
Fluents will usually be persistent, as specified by persistence statements of theform:∀t, x [Per (t, f (x))]
Finally, the values of fluents at the start of the planning process are (completely) specified using observations at timepoint zero of the form:[0] f =
ˆ v
where v is a constant. In order to make these general forms more concrete
they will be accompanied by a running example consisting of the UAV logistics scenario fragment from Section 3.3. Again, the example consists of anaction attach, used by a UAV to attach a crate that can then be moved toanother location. The action specification involves a location-valued fluent
loc(object), representing the location of an object, and a boolean-valued fluent
carrying(uav,crate) that is true whenever the UAV given as the first argument
is carrying the crate in the second argument. The attach action will make thecarrying fluent true and the value of the loc fluent unspecified given that the
UAV remains in the same location as the crate during the execution of theaction. The L(ND) specification is given by:4.2. Translation from L(ND) to L(FL)29[t1 , t2 ] attach(u, c)∀l [[t1 ] loc(c) =ˆ l ∧ [t1 , t2 ] loc(u) =ˆ l→R((t1 , t2 ] carrying(u, c)) ∧ R((t1 , t2 ] ¬loc(c) =ˆ l)]Both carrying and loc are persistent fluents:∀t, o [Per (t, loc(o))]∀t, u, c [Per (t, carrying(u, c))]Finally, an initial state is set up. We introduce a fluent pos that can be used
to refer to locations using coordinates, e.g. as follows:[0] loc(uav1) =ˆ pos(300, 90)[0] loc(crate1) =ˆ pos(300, 90)[0] ¬carrying(uav1, crate1)

4.2

Translation from L(ND) to L(FL)The first step in translating the above L(ND) narrative to an executable logic
program is to use the transformation function Trans to compile the narrative
into the first-order logic language L(FL). Using the definition of Trans given in
Section 2.3.1, augmented with the reified action occurrences argument p, theaction specifications (1) are translated into:∀t1 , t2 , w, p [t1 < t2 ∧ Occurs(t1 , t2 , a(w), p) → ∀x [P (y) → E(z)]](2)

Each condition in the conjunction P (y) has been translated into:
Holds(t1 , f (y), v, p)
or to ∀t [t1 ≤ t ≤ t2 → Holds(t, f (y), v, p)] if the condition was specified to holdthroughout the entire action interval by supplying an end timepoint t2 . Eachreassignment in the conjunction E(z) is translated into:(¬)Holds(t2 , f (z), v, p) ∧ ∀t [t1 < t ≤ t2 → Occlude(t, f (z), p)]
Persistence statements are instantiations of the general persistence formula for
a given fluent f , with the addition of the action occurrence argument:∀t, x, p [¬Occlude(t + 1, f (x), p) →∀v [Holds(t, f (x), v, p) ↔ Holds(t + 1, f (x), v, p)]]Each initial fluent value observation becomes:∀p [Holds(0, f, v, p)]

30

Compiling TAL into Logic Programs

Finally, the Occurs predicate for reified action occurrences was defined in Section 3.1 as:∀t1 , t2 , a, p [Occurs(t1 , t2 , a, p) ↔ Member (occ(t1 , t2 , a), p)](3)

Returning to the example from the UAV logistics narrative fragment, its action
specification, persistence statements, and initial state observations are translated into the following set of formulas:∀t1 , t2 , u, c, l, p [t1 < t2 ∧ Occurs(t1 , t2 , attach(u, c), p) →Holds(t1 , loc(c), l, p) ∧ ∀t [t1 ≤ t ≤ t2 → Holds(t, loc(u), l, p)] →Holds(t2 , carrying(u, c), true, p) ∧∀t [t1 < t ≤ t2 → Occlude(t, carrying(u, c), p)] ∧¬Holds(t2 , loc(c), l, p) ∧∀t [t1 < t ≤ t2 → Occlude(t, loc(c), p)]]∀t, x, p [¬Occlude(t + 1, loc(x), p) →∀v [Holds(t, loc(x), v, p) ↔ Holds(t + 1, loc(x), v, p)]]∀t, u, c, p [¬Occlude(t + 1, carrying(u, c), p) →∀v [Holds(t, carrying(u, c), v, p) ↔ Holds(t + 1, carrying(u, c), v, p)]]∀p [Holds(0, loc(uav1), pos(300, 90), p)]∀p [Holds(0, loc(crate1), pos(300, 90), p)]∀p [Holds(0, carrying(uav1, crate1), false, p)]

4.3

Introducing Interval Occlusion

The second step consists of obtaining a definition of timepoint occlusion specificto the given narrative and then replacing it by an equivalent definition of interval occlusion. To accomplish this we split the action specification formulas,each of the form (2), into fluent value reassignments and occlusion formulas.
The occlusion predicates are then collected into a single Occlude predicate using
the equivalence:Φ(f1 ) ∧ · · · ∧ Φ(fn ) ≡ ∀x [(x = f1 ∨ · · · ∨ x = fn ) → Φ(x)](4)

The resulting form is:∀t1 , t2 , w, x, p [t1 < t2 ∧ Occurs(t1 , t2 , a(w), p) ∧ P (y) → E 0 (z)]∀t, f, t1 , t2 , w, x, p [t1 < t ≤ t2 ∧ Occurs(t1 , t2 , a(w), p) ∧ P (y) ∧(f = f1 (z) ∨ · · · ∨ f = fn (z)) →Occlude(t, f, p)]

(5)
(6)

where E 0 are the reassignments without the occlusion sub-formulas. Applying
this rewrite to the example attach action specification produces:

4.3. Introducing Interval Occlusion∀t1 , t2 , u, c, l, p [t1 < t2 ∧ Occurs(t1 , t2 , attach(u, c), p) ∧Holds(t1 , loc(c), l, p) ∧ ∀t [t1 ≤ t ≤ t2 → Holds(t, loc(u), l, p)] →Holds(t2 , carrying(u, c), true, p) ∧ ¬Holds(t2 , loc(c), l, p)]∀t, f, t1 , t2 , u, c, l, p [t1 < t ≤ t2 ∧ Occurs(t1 , t2 , attach(u, c), p) ∧Holds(t1 , loc(c), l, p) ∧ ∀t [t1 ≤ t ≤ t2 → Holds(t, loc(u), l, p)] ∧(f = carrying(u, c) ∨ f = loc(c)) →Occlude(t, f, p)]

31

(7)

To be able to conveniently prove persistency over qualitative time intervals
we would like to express these timepoint occlusion formulas using interval occlusion. The definition of interval occlusion in terms of timepoint occlusion,
repeated here with the additional argument for reified action occurrences, is:∀t1 , t2 , f, p [Occlude(t1 , t2 , f, p) ↔ ∃t [t1 < t ≤ t2 ∧ Occlude(t, f, p)]](8)

Before this definition can be applied we need to put the occlusion formulas (6)into a form where they contain the sub-formula ∃t[t1 < t ≤ t2 ∧Occlude(t, f, p)].
According to (8) this is equivalent to, hence can be replaced by, interval occlusion. The following equivalence, proven in Appendix B.3, serves this purpose:∀t [Φ(t) → Ψ(t)] ≡∀t1 , t2 [∃t [t1 < t ≤ t2 ∧ Φ(t)] → ∃t [t1 < t ≤ t2 ∧ Ψ(t)]](9)

Let the antecedent and consequent of the occlusion implication (6), with t1 andt2 renamed to t3 and t4 , be Φ and Ψ as in:def

Φ(t) = t3 < t ≤ t4 ∧ Occurs(t3 , t4 , a(w), p) ∧ P (y) ∧(f = f1 (z) ∨ · · · ∨ f = fn (z))defΨ(t) = Occlude(t, f, p)
Then the occlusion formula (6) is rewritten according to theorem (9) as:∀t1 , t2 , t3 , t4 , f, w, x, p [∃t [t1 < t ≤ t2 ∧ t3 < t ≤ t4 ∧Occurs(t3 , t4 , a(w), p) ∧ P (y) ∧(f = f1 (z) ∨ · · · ∨ f = fn (z))] →∃t [t1 < t ≤ t2 ∧ Occlude(t, f, p)]]
The right hand side of the implication is now in the form required for the application of definition (8). Replacing it and reducing the scope of the existential
quantifier on the left hand side results in:∀t1 , t2 , t3 , t4 , f, w, x, p [∃t [t1 < t ≤ t2 ∧ t3 < t ≤ t4 ] ∧Occurs(t3 , t4 , a(w), p) ∧ P (y) ∧(f = f1 (z) ∨ · · · ∨ f = fn (z)) →Occlude(t1 , t2 , f, p)]

32Compiling TAL into Logic Programs

The sub-formula ∃t [t1 < t ≤ t2 ∧ t3 < t ≤ t4 ] expresses the existence of ashared point between the intervals (t1 , t2 ] and (t3 , t4 ]. One can construct thecorresponding interval algebra relation {o, s, d, f, =, f i, di, si, oi} by collecting
all primitive interval relations that express some form of overlapping. Using
the end-point comparison tree described by Thornton et. al. [38] this seemingly
complex relation can be simplified to the end-point comparison t2 > t3 ∧t1 < t4 .
To point out the correspondence between the existentially quantified timepoint
sub-formula and the end-point comparison definition of interval overlap, provedin Appendix B.4, we will make use of a new predicate Overlap, defined asfollows:∀t1 , t2 , t3 , t4 [t2 > t3 ∧ t1 < t4 ↔ Overlap(t1 , t2 , t3 , t4 )]Introducing the Overlap predicate into the occlusion formula puts all occlusion
formulas into the general form:∀t1 , t2 , t3 , t4 , f, w, x, p [Overlap(t1 , t2 , t3 , t4 ) ∧Occurs(t3 , t4 , a(w), p) ∧ P (y) ∧(f = f1 (z) ∨ · · · ∨ f = fn (z)) →Occlude(t1 , t2 , f, p)](10)

The specific form of the example attach occlusion formula is:∀t1 , t2 , t3 , t4 , f, u, c, l, p [Overlap(t1 , t2 , t3 , t4 ) ∧Occurs(t3 , t4 , attach(u, c), p) ∧Holds(t3 , loc(c), l, p) ∧∀t [t3 ≤ t ≤ t4 → Holds(t, loc(u), l, p)] ∧(f = carrying(u, c) ∨ f = loc(c)) →Occlude(t1 , t2 , f, p)](11)

To complete the transformation to interval occlusion, and take advantage ofthe possibility to prove a fluent persistent over an entire temporal interval, thepersistence formulas must be replaced by formulas of the same form as formula(3) in Section 3.2 but including the action occurrence argument:∀t1 , t2 , x, p [t1 < t2 ∧ ¬Occlude(t1 , t2 , f (x), p) →∀v [Holds(t1 , f (x), v, p) ↔ Holds(t2 , f (x), v, p)]]

4.4

(12)

Transformation to Horn Form

The third translation step rewrites formulas into Horn clause form. The reassignment part of action specifications (5) is now of the general form:

4.4. Transformation to Horn Form

33

t1 < t2 ∧ Occurs ∧ P1 ∧ · · · ∧ Pm → E10 ∧ · · · ∧ En0
where, as before, each Pi is a condition and each Ej0 is a reassignment without
the occlusion part. Each such formula is expanded into the implications:t1 < t2 ∧ Occurs ∧ P1 ∧ · · · ∧ Pm → E10
..
.

(13)

t1 < t2 ∧ Occurs ∧ P1 ∧ · · · ∧ Pm → En0
This is in Horn form except for those conditions Pi that were specified to holdover the whole action occurrence interval [t1 , t2 ], which are still of the complex
form:∀t [t1 ≤ t ≤ t2 → Holds(t, f (y), v, p)]
For persistent fluents this is equivalent to f (y) holding the value v at the first
timepoint t1 and, by virtue of not being occluded at any timepoint during theinterval, the value v persisting until timepoint t2 :Holds(t1 , f (y), v, p) ∧ ¬∃t [t1 < t ≤ t2 ∧ Occlude(t, f (y), p)]
According to the definition of interval occlusion (8) this is simply:
Holds(t1 , f (y), v, p) ∧ ¬Occlude(t1 , t2 , f (y), p)(14)

The occlusion formulas (10) are in Horn form except for the disjunction overfluents. Rewriting the formula by distributing conjunction over the fluent disjunction, and then distributing the resulting conjunction over the implication,
results in one implication for each equality f = fi (z). Applying equivalence(4) in the left direction to each implication results in one occlusion definition
for each fluent:∀t1 , t2 , t3 , t4 , w, x, p [Overlap(t1 , t2 , t3 , t4 ) ∧ Occurs(t3 , t4 , a(w), p) ∧ P (y) →Occlude(t1 , t2 , f1 (z), p)]..
.
∀t1 , t2 , t3 , t4 , w, x, p [Overlap(t1 , t2 , t3 , t4 ) ∧ Occurs(t3 , t4 , a(w), p) ∧ P (y) →Occlude(t1 , t2 , fn (z), p)]
Each of these formulas contain the action conditions P (y). This reflects the factthat attempting to execute an action when its conditions are not satisfied will
have no effect. We will perform an additional simplification on the occlusion
formulas by removing these conditions. In our application, the synthesis andreasoning about plans and actions to execute in the future, considering actions
that are not executable is not really relevant. When only considering actions

34

Compiling TAL into Logic Programs

that can actually be executed this simplification has no effect on the results.
Each simplified occlusion formula is then of the form:∀t1 , t2 , t3 , t4 , w, x, p [Overlap(t1 , t2 , t3 , t4 ) ∧ Occurs(t3 , t4 , a(w), p) →Occlude(t1 , t2 , f (z), p)](15)

Returning to the example logistics narrative fragment, the occlusion formula(11) is instantiated over the fluents carrying and loc, and simplified by ignoring
the conditions for executing the action:∀t1 , t2 , t3 , t4 , u, c, p [Overlap(t1 , t2 , t3 , t4 ) ∧ Occurs(t3 , t4 , attach(u, c), p) →Occlude(t1 , t2 , carrying(u, c), p)]∀t1 , t2 , t3 , t4 , u, c, p [Overlap(t1 , t2 , t3 , t4 ) ∧ Occurs(t3 , t4 , attach(u, c), p) →Occlude(t1 , t2 , loc(c), p)]
To complete the transformation to Horn clause form we need to deal with theequivalence in persistence statements (12) and the Occurs definition (3). Bothcan be rewritten in the form of two implications, however, in each case only
one direction is of interest. Persistence will only be proved forward in time,and occurrences are only proved from the occurrence set argument. These
implications are then in Horn form:∀t1 , t2 , x, v, p [t1 < t2 ∧ ¬Occlude(t1 , t2 , f (x), p) ∧Holds(t1 , f (x), v, p) →Holds(t2 , f (x), v, p)]∀t1 , t2 , a, p [Member (occ(t1 , t2 , a), p) → Occurs(t1 , t2 , a, p)]

4.5

(16)

(17)

Circumscription Policy

Before moving on to the encoding of the formulas as logic programming clauses
we need to clarify the relation between the current state of the formulas and the
TAL circumscription policy, which was defined in Section 2.5. It is designed tocapture the commonsense intuition that change does not spontaneously happen
unless there is some reason for it. E.g. if the UAV does not fly anywhere then,by default, its location is unchanged. More formally, given a suitable TAL
narrative describing the workings of the UAV, we would like to conclude thatthe value of the UAV’s location fluent will persist over a time interval, unless
we in fact know that the UAV was involved in some flying activity during theinterval.
In practice, restrictions on the form of TAL narratives ensure that thecircumscription policy is reducible to predicate completion, even in the general4.6. Clauses and Rules

35

case without our additional restrictions added to ensure a proper translation
into constraint logic programs. In the compilation above, the occlusion formulas
are already in a form amenable to completion by replacing the implications byequivalences, which is the standard way of circumscribing Occlude and Occurs
in the first-order version of TAL narratives. In the case of our logic program
encoding, predicate completion can be viewed as the declarative semantics ofthe negation as failure mechanism of logic programs. This fact suggests that
we should leave the occlusion formulas as they are and rely on the “built-in”
completion of Prolog to implement the circumscription policy.
However, the situation is complicated when one considers planning. Thereis no action sequence given beforehand that determines occlusion once and forall. On the contrary, the occlusion concept is continually used to prove fluent value persistence while, at the same time, actions are added to the reified
action occurrence set that might affect and modify the very same occlusion.
Consequently, we need to continually ensure that considered actions do not violate any persistence proofs that have already been assumed. The Constraint
Handling Rules (CHR) framework [10] together with the use of temporal constraint formalisms make a flexible solution to this problem possible. By expressing occlusion using constraint handling rules instead of Prolog clauses we
ensure that the conditions are automatically reevaluated whenever needed. The
next section presents these rules and explains how they implement a dynamic
action/persistence conflict resolution.
Finally, action occurrences should also be circumscribed. Since occlusion
will be represented by constraint handling rules, and occlusion depends on action occurrences, we will need to express action occurrences as constraints too.
Every time an action is added to the action occurrence set, passed around in thep argument, we will also add it to the constraint store. While the action occurrence argument represents a possibly incompletely specified action sequence,the constraint store is implicitly closed. Therefore the collection of action occurrences added to the store serves as a representation of the circumscriptionof Occurs.

4.6

Clauses and Rules

The fourth and final translation step encodes the TAL formulas as Prolog
clauses, constraint handling rules, and finite domain constraints. We startwith the Occurs definition (17):occurs(T1,T2,A,P) :member(occ(T1,T2,A),P), circ occurs(T1,T2,A).

36

Compiling TAL into Logic Programs

member(A,[A|Pp]).
member(A,P) :nonvar(P), P = [A1|P1], A \== A1, member(A,P1).
This deviates from a literal translation into Prolog in two ways. First, thecirc occurs constraint was added to make sure the action occurrence is present
in the constraint store, where it can interact with the constraint handling rules
for occlusion, as noted in Section 4.5. Second, the member predicate uses Prolog’s built in list syntax rather than the cons function, introduced in Section 3.1.
Though our implementation of member is not the same as the standard one provided by the Prolog list library. The reason is that if one adds an action, andis subsequently forced to backtrack due to reaching a dead end in the search
space, then the library version supplies an infinite number of irrelevant backtracking possibilities. Instead of trying some other action, one would be stuckconsidering syntactically alternative ways of adding the same action to the list.
Action occurrence terms should be collected in a set, without consideration of
their syntactic order. This is the behaviour of the fluent composition function ◦,used to represent world states in the Fluent Calculus [37]. Our implementationof member borrows Thielscher’s fluent composition predicate holds from the
Fluent Calculus FLUX system [36], which provides only relevant backtracking
opportunities.
Next, each of the n action reassignment formulas in (13) is of the form:∀t1 , t2 , w, x, p [t1 < t2 ∧ Occurs(t1 , t2 , a(w), p) ∧Holds(t1 , f1 (y1 ), v1 , p) ∧ · · · ∧ Holds(t1 , fm (ym ), vm , p) →Holds(t2 , f (z), v, p)]with, according to (14), a ¬Occlude(t1 , t2 , fi (y), p) for those conditions thatshould persist over the entire action occurrence interval. This is written as a
Prolog clause:holds(T2,f (z),v,P) :types(x), T1 #< T2, occurs(T1,T2,a(w),P),
holds(T1,f1 (y1 ),v1 ,P), · · · , holds(T1,fm (ym ),vm ,P).
with the addition of not occlude(T1,T2,fi (y),P) for persisting conditions.
Since the timepoints t1 and t2 are usually not instantiated as integers, theinequality between them can not be expressed by Prolog’s built-in arithmetic
operator. Instead the inequality is added to the finite domain constraint solver
store using #<. Finally, L(FL) is an order-sorted logic that may associate type
restrictions on fluent arguments. Prolog is not typed, but the types predicate
is expanded into unary type clauses that ensure that action argument variables
only take on values from the value domain that corresponds to their type. For

4.6. Clauses and Rules

37

example, the action of attaching crates involves a variable c ranging over theset of crates. The Prolog translation of its action reassignment formula would
include a unary predicate crate(C), and the set of crates that the variable
ranges over would be added to the program as assertions:crate(crate1).
crate(crate2).
crate(crate3).
A special timepoint type predicate ensure that the timepoint variables T1 andT2 are assigned a finite domain, as required by the finite domain constraint
solver.
Before moving on, note that Prolog does not have classical negation. Consequently negative effects, such as ¬Holds(t2 , loc(c), l, p) in our attach example,
can not be encoded explicitly in the logic program. Negation is implicit in theassumption of complete knowledge and negation as failure. Thus, if a fluent
has not been explicitly mentioned in the effects of some action, it can be provenfalse using negation as failure. One might wonder whether persistence would
not allow propagating a fluent’s value from some earlier timepoint, even in thepresence of an intermediate action with the negation of the fluent among its
effects, since that intermediary negative effect is not explicitly encoded. However, the fluent is still explicitly occluded, as specified by the occlusion part of
the action specification. Any action that occludes the fluent while overlapping
the persistence interval will, by the definition of interval occlusion, also occlude
the persistence interval, and persistence will not be applicable.
Once again returning to the logistics example, the negative effect of attach
in formula (7) is accordingly left out of the logic program while the positiveeffect, which is of the form:∀t1 , t2 , u, c, l, p [t1 < t2 ∧ Occurs(t1 , t2 , attach(u, c), p) ∧Holds(t1 , loc(c), l, p) ∧ Holds(t1 , loc(u), l, p) ∧¬Occlude(t1 , t2 , loc(u), p) →Holds(t2 , carrying(u, c), true, p)]
is compiled into:
holds(T2,carrying(U,C),true,P) :uav(U), crate(C), timepoint(T1), timepoint(T2),
T1 #< T2, occurs(T1,T2,attach(U,C),P),
holds(T1,loc(C),L,P), holds(T1,loc(U),L,P),
not occlude(T1,T2,loc(U),P).

38

Compiling TAL into Logic Programs

where uav/1 and crate/1 are the type predicates that prevent the action frombeing applied to anything else than UAVs and crates, and timepoint/1 assign
finite domains to the timepoint variables.
According to the declarative CHR semantics (page 7, [10]), each occlusion
formula of the form (15), repeated here:∀t1 , t2 , t3 , t4 , w, x, p [Overlap(t1 , t2 , t3 , t4 ) ∧ Occurs(t3 , t4 , a(w), p) →Occlude(t1 , t2 , f (z), p)]
is equivalent to a constraint handling rule of the following form:
overlap(T1,T2,T3,T4), occurs(T3,T4,a(w),P) ==>occlude(T1,T2,f (x),P).
The purpose of this rule is to occlude fluents that are affected by action occurrences in the action occurrence set p. While planning, however, the set
p is intentionally incompletely specified to allow the addition of new actions.
Whether or not some specific action is present in the current action occurrence set p may not be known, and supplying the corresponding Prolog goal
occurs(T3,T4,a(w),P) would actually add the action if not already present,
since this is a valid way of proving that goal. The same problem applies to the
occlusion constraint on the right hand side of the rule since it also depends on
the actions occurrence set. The best we can do is to make sure that fluentsaffected by actions that we have assumed occur, up to the current point in theplanning process, are occluded. Those actions are stored using the circ occurs
constraint, as noted in the translation of the Occurs definition (17). By replacing the use of predicates that depend on the incompletely specified set P by
the corresponding constraints, circ occurs and occlude, we take all actions
that are currently in the plan into consideration. The CHR framework thenassumes responsibility for the rest of the work by continually monitoring these
constraints for updates. Whenever the action occurrence set P is modified, a
new circ occurs constraint is added, and the occlusion rule is automaticallyreevaluated. The new constraint handling rule is then:overlap(T1,T2,T3,T4), circ occurs(T3,T4,a(w)) ==>occlude(T1,T2,f (x)).
The persistence formulas are of the form (16), repeated here:∀t1 , t2 , x, v, p [t1 < t2 ∧ ¬Occlude(t1 , t2 , f (x), p) ∧ Holds(t1 , f (x), v, p) →Holds(t2 , f (x), v, p)]
and are encoded as prolog clauses:(18)

4.6. Clauses and Rules

holds(T2,f (x),v,P) :timepoint(T1), timepoint(T2), T1 #< T2,
not occlude(T1,T2,f (x)), holds(T1,f (x),v,P).

39

(19)

The negated Occlude predicate is encoded as a constraint not occlude to allow
the proper interaction with the occlude constraint in the occlusion CHR rule(18). As before, the best we can do is to consider all decisions made up to thecurrent point in the planning process. CHR will then remember to reevaluate
the rules whenever new descisions are made. Specifically, when the persistence
formula (19) is used to propagate a fluent’s value, the not occlude constraint
would be added to the constraint store. If an overlapping action interval that
affects the fluent’s value was already present in the store, the fluent would not
really be persistent. The occlusion rule (18) should be reevaluated and detect
the conflict, adding a contradictory occlude constraint to the store. The only
missing piece is a rule to force backtracking when such conflicts, caused by apersistence assumptions and action occurrences, are detected:
not occlude(T1,T2,f (x)), occlude(T1,T2,f (x)) ==> fail.
However, there is one problem with this initial encoding attempt and it is related to the overlap constraint. The CHR rule (18) is a syntactic matchingrule. It will only trigger if the constraints on its left hand side are explicitly
represented in the constraint store. Action occurrences are stored explicitly
in the circ occurs constraint, but the same is not true for the overlap constraint. Unless we have complete knowledge about the ordering of actions andrepresent this knowledge as explicit constraints, the rule may not trigger todetect conflicts between persistence assumptions and actions that are added
to the plan. But we would like to have both a compact and incomplete representation of temporal constraints. This would allow the implementation tofollow a strategy of least commitment concerning the orderings of actions andto generate partially ordered plans.
Solving this problem involves restructuring the occlusion formulas so thatknowledge of interval overlap is not a prerequisite to conflict detection, but aconsequence. The occlude formulas (15) have their relations rearranged into
the logically equivalent form:∀t1 , t2 , t3 , t4 , w, x, p [¬Occlude(t1 , t2 , f (z), p) ∧ Occurs(t3 , t4 , a(w), p) →¬Overlap(t1 , t2 , t3 , t4 )]Likewise, the new constraint handling rule, replacing (18), is:not occlude(T1,T2,f (x)), circ occurs(T3,T4,a(w)) ==>not overlap(T1,T2,T3,T4).

40

Compiling TAL into Logic Programs

Both the not occlude and circ occurs constraints have complete representations in the constraint store, thereby ensuring that the rule will trigger
whenever these constraints are modified in the store. Thus, when clause (19)has been used to prove a fluent persistent over an interval (t1 , t2 ], adding a
not occlude constraint in the process, and an action that threatens to modify
the fluent occurs during interval (t3 , t4 ], then the rule will act to constrain thetwo intervals not to overlap. The not overlap predicate adds the corresponding interval algebra end-point constraints to the finite domain constraint solver
discussed in Section 3.2.1. If the addition of these temporal constraints results
in inconsistency, Prolog will backtrack, forcing the choice of another actionor the removal of the persistence assumption. In other words, the mechanism
resolves threats posed by actions, which could potentially disturb fluents thatare required to be persistent, by introducing restrictions on the order of actions
and persistence intervals. Backtracking is only necessary when further ordering
restrictions are not possible.
In the logistics example the resulting persistence clauses and occlusion rules
are as follows:
holds(T2,carrying(U,C),V,P) :timepoint(T1), timepoint(T2), T1 #< T2,
not_occlude(T1,T2,carrying(U,C)),
holds(T1,carrying(U,C),V,P).
holds(T2,loc(C),V,P) :timepoint(T1), timepoint(T2), T1 #< T2,
not_occlude(T1,T2,loc(C)),
holds(T1,loc(C),V,P).
not_occlude(T1,T2,carrying(U,C)),
circ_occurs(T3,T4,attach(U,C)) ==>not_overlap(T1,T2,T3,T4).
not_occlude(T1,T2,loc(C)),
circ_occurs(T3,T4,attach(U,C)) ==>not_overlap(T1,T2,T3,T4).
Finally, observation statements are easily encoded as:holds(0,f ,v,P).
In the case of the UAV example the encoding is:holds(0,loc(uav1),pos(300,90),P).
holds(0,loc(crate1),pos(300,90),P).

4.7. Summary

41

The compilation results in executable constraint logic programs for deductiveplanning and reasoning. An example program is integrated with the UAV
system in Chapter 5 and listed in full in the Appendix.

4.7

Summary

Although many translation steps are equivalence preserving, some are necessarily not, or else we would not have arrived at a logic program with deductiveplanning capability. We summarize the points of difference here.
• An obvious restriction on the original TAL is the form of L(ND) input
theories, which limits the applicability of the compilation to domainsthat can be adequately described while satisfying these constraints. The
translation from L(ND) to the first-order L(FL) is unmodified. Instead,additional translations are subsequently performed.
• Timepoint occlusion is replaced by interval occlusion in the action specifications. Interval occlusion is defined in terms of TAL’s original timepoint
occlusion by (8), and the modification is expressed in terms of an equivalence preserving rewrite (Appendix B.3).
• Interval overlap is expressed succinctly using an Overlap predicate thatis equivalent to the formula expressing interval overlap that resulted fromthe translation to interval occlusion (Appendix B.4).
• A formula (12) that allows the use of fluent persistency over intervals of
any length is added. It is entailed by the definition of interval occlusionand persistence (Appendix B.1, Appendix B.2), but is weaker than theinterval persistence formula (2) in Section 3.2 since it does not (by itself)
constrain the fluent’s value during the interval. The stronger formula
could presumably be added, if needed, but we have not investigated thisfurther.
• The formulas are expanded into equivalent formulas in Horn form, whichis possible due to the restrictions on the original L(FL) narrative. An
additional requirement is that fluents that are specified to hold a specificvalue throughout the action occurrence interval are persistent. Otherwise
one would need to use universal quantification over timepoints in thatinterval.
• Occlusion formulas are significantly simplified by removing the action
preconditions (which are independently present in action effect formulas).

42

Compiling TAL into Logic Programs

This weakens the theory since actions may occlude fluents, preventing
application of persistence, even though the actions may in fact have had
no effects due to their preconditions not being satisfied. Though, whenplanning, such cases will never actually appear since it would be pointless
to add actions without effects to the narrative.
• When the persistence equivalence (12) is turned into a Horn form implication, this weakens the theory to persistence forward in time. We havenot investigated whether the other direction could be included to allow
postdictive conclusions about fluent values at earlier timepoints based on
knowledge about later timepoints.
• CHR rules minimize occlusion and occurrences in the same way the circumscription policy would have done, from a theoretical point of view.
However, the difference is that the proof mechanism is applicable even toa dynamically changing narrative, which is the case in deductive planning.
• The conversion of the Horn formulas into Prolog clauses strengthens thetheory in the sense that anything that was previously unknown is now
false. But it limits the applicability of our methods, as noted below.
• Finally, the use of a finite domain constraint solver for (in)equalities weakens the theory since we can not draw conclusions e.g. about fluent values
outside the bounded time line. In practice this problem can be circumvented by adjusting the size of the bound.
The generated constraint logic programs are thus associated with severe
restrictions on the form of TAL theories that can be used as input. Specifically,
the requirement of a completely specified initial state and the negation-asfailure semantics of Prolog make the compilation, as it is described above,inapplicable to planning problems that involve incomplete information, andthe restrictions imposed by Horn-clause form limit syntactic expressivity andthe use of quantifiers.
It is important to note, however, that without some mechanism for incremental minimization of Occlude and Occurs, deductive planning would be
impossible. Previous work with TAL (e.g. the most recent language specification [8] and the most used reasoning tool [18]) has assumed the provisionof completely specified narratives, detailing what actions occur when, before
any reasoning process commences. The constraint handling rules, introduced
above, take care of the minimization in an automated fashion and allow the
dynamic generation of new narratives. They significantly simplify the proof
process and make automated planning efficient. Building on this basis will

4.7. Summary

43

require augmentation of the basic Prolog inference mechanism through a metainterpreter, or replacing Prolog with a more powerful theorem prover, but such
efforts should ultimately benefit from the inherent capability of the underlying
TAL language to compactly represent incompletely specified information, andmake possible a more liberal use of quantifiers.

44

Compiling TAL into Logic Programs

Chapter 5

Composite Actions
The previous chapters have considered plans in the form of sets of primitive
action occurrences that are partially ordered on a time line. But such a view
is not sufficiently general to capture the entire range of plans that we would
intuitively expect an intelligent agent to be able to use. Specifically, there is noconcept of conditional action occurrences or of repetition of action occurrences.
If such constructs are introduced they form a basic scripting language that canbe used to express more complex instructions for the agent to carry out.
This chapter extends the high-level L(ND) lanugage syntax to cover sequences of action occurrences, conditional occurrences, nondeterministic choiceactions, and loops. A semantics for these composite actions is provided by acorresponding extension of the Trans function that translates the high-level
language into the first-order language L(FL). The result, however, is no longer
a first-order language. A move to fixpoint logic is necessary since we make useof the least fixpoint operator to capture the semantics of loop constructs. Finally, a compilation of composite actions into Prolog clauses is described, which
permits the execution of complex actions in the logic programming frameworkthat was developed in Chapter 4.

5.1

Syntax and Semantics

The syntax and semantics of composite actions are defined by extending thetranslation function Trans defined in Section 2.3.1. The following additions
illustrate both the L(ND) syntax of composite actions and the result of translating them to L(FL) with the least fixpoint operator. Let a be a primitive
action, C a formula expressing some condition, and A a composite action. We
45

46

Composite Actions

extend Trans with sequences, conditional action occurrences, non-deterministic
choice, and loops as follows:defTrans([t1 , t2 ] A1 ; A2 ) =∃t[t1 < t < t2 ∧Trans([t1 , t] A1 ) ∧Trans([t, t2 ] A2 )]def

Trans([t1 , t2 ] if C then A) =Trans([t1 ] C) → Trans([t1 , t2 ] A)
def

Trans([t1 , t2 ] choose x A) =∃x[Trans([t1 , t2 ] A)]

def

Trans([t1 , t2 ] do A until C) =µX(x, y)[Trans([x] ¬C) → ∃z[x < z ≤ y ∧Trans([x, z] A) ∧ X(z, y)]](t1 , t2 )5.2

Fixpoint Expansion

Although the semantics of the first three composite actions is relatively self
explanatory, it might not be immediately obvious what the fixpoint formula in
the fourth case means. A least fixpoint formula is of the general form:µX(x)[Φ](t)where X is k-ary relational variable, x is k variables, and Φ is a formula with
only positive occurrences of X. Variables in x that are unbound in Φ serve
as arguments for the fixpoint function and their values are provided in t. The
semantics of the expression can be defined model-theoretically as a least fixpoint
relation on sets. However, we will instead illustrate its meaning using thefollowing syntactic expansion theorem:

_
false
if i = 0iiµX(x)[Φ](t) ≡ [ X ](t) where X ≡Φ[X(x) ← X i−1 (x)] otherwisei∈Z

The fixpoint formula can thus be rewritten as an (infinite) disjunction where
each disjunct is an expansion of the formula Φ with occurrences of X replacedby the previous expansion step.

5.2.1

Expansion Example

Consider a UAV logistics task where there is a need for a certain number ofcrates at a specific location. We would like to instruct the UAV to start delivering crates at timepoint s and stop at some later time t when a sufficientnumber of crates are available at the target location. For the purpose of illustration we help keep the formulas relatively lucid by abridging the delivery5.2. Fixpoint Expansion

47

of a crate as an action deliver and the condition to be satisfied as a boolean
fluent sufficient. A composite action to accomplish the given task would thenbe written as:[s, t] do deliver until sufficient =ˆ trueAccording to the extended Trans function defined above, this macro is expanded into the fixpoint L(FL) formula:µX(x, y)[¬Holds(x, sufficient, true) →∃z [x < z ≤ y ∧ Occurs(x, z, deliver) ∧ X(z, y)]](s, t)
The first step of the expansion, X 0 , is simply false. The next step, X 1 , isobtained by replacing the occurrence of X in the body of the fixpoint formulawith X 0 (which is false). The result is rewritten in disjunctive form to help
illustrate a uniform structure that will become clear after a couple of expansion
steps:¬Holds(x, sufficient, true) →∃z [x < z ≤ y ∧ Occurs(x, z, deliver) ∧ X 0 (z, y)] ≡Holds(x, sufficient, true) ∨∃z [x < z ≤ y ∧ Occurs(x, z, deliver)]
Again, replacing X by X 1 in the fixpoint formula body and rewriting resultsin X 2 :¬Holds(x, sufficient, true) →∃z [x < z ≤ y ∧ Occurs(x, z, deliver) ∧ X 1 (z, y)] ≡Holds(x, sufficient, true) ∨∃z [x < z ≤ y ∧ Occurs(x, z, deliver) ∧(Holds(z, sufficient, true) ∨ ∃z2 [z < z2 ≤ y ∧ Occurs(z, z2 , deliver)])] ≡Holds(x, sufficient, true) ∨∃z [x < z ≤ y ∧ Occurs(x, z, deliver) ∧ Holds(z, sufficient, true)] ∨∃z, z2 [x < z < z2 ≤ y ∧ Occurs(x, z, deliver) ∧ Occurs(z, z2 , deliver)]The structure of the formula becomes more clear when completing the third
step, replacing X by X 2 and rewriting to get X 3 :¬Holds(x, sufficient, true) →∃z [x < z ≤ y ∧ Occurs(x, z, deliver) ∧ X 2 (z, y)] ≡48

Composite Actions

Holds(x, sufficient, true) ∨∃z [x < z ≤ y ∧ Occurs(x, z, deliver) ∧(Holds(z, sufficient, true) ∨∃z2 [z < z2 ≤ y ∧ Occurs(z, z2 , deliver) ∧ Holds(z2 , sufficient, true)] ∨∃z2 , z3 [z < z2 < z3 ≤ y ∧Occurs(z, z2 , deliver) ∧ Occurs(z2 , z3 , deliver)])] ≡Holds(x, sufficient, true) ∨∃z [x < z ≤ y ∧ Occurs(x, z, deliver) ∧ Holds(z, sufficient, true)] ∨∃z, z2 [x < z < z2 ≤ y ∧ Occurs(x, z, deliver) ∧Occurs(z, z2 , deliver) ∧ Holds(z2 , sufficient, true)] ∨∃z, z2 , z3 [x < z < z2 < z3 ≤ y ∧ Occurs(x, z, deliver) ∧Occurs(z, z2 , deliver) ∧ Occurs(z2 , z3 , deliver)]The expansion continues indefinitely but the general form of the resulting disjunction is clear:
Holds(x, sufficient, true) ∨∃z [x < z ≤ y ∧Occurs(x, z, deliver) ∧Holds(z, sufficient, true)] ∨∃z, z2 [x < z < z2 ≤ y ∧Occurs(x, z, deliver) ∧Occurs(z, z2 , deliver) ∧Holds(z2 , sufficient, true)] ∨∃z, z2 , z3 [x < z < z2 < z3 ≤ y ∧Occurs(x, z, deliver) ∧Occurs(z, z2 , deliver) ∧Occurs(z2 , z3 , deliver) ∧Holds(z3 , sufficient, true)] ∨∃z, z2 , z3 , z4 [x < z < z2 < z3 < z4 ≤ y ∧Occurs(x, z, deliver) ∧Occurs(z, z2 , deliver) ∧Occurs(z2 , z3 , deliver) ∧Occurs(z3 , z4 , deliver) ∧Holds(z4 , sufficient, true)] ∨ · · ·The above formula corresponds to the expected behaviour of the composite
loop action. Each disjunct represents an additional occurrence of the deliveraction in the series before the sufficient condition is satisfied. The unfoldingof the composite loop action (in the context of a narrative that specifies theeffects of the action, the initial conditions, and the sufficient condition) is given5.3. Compiling Composite Actions

49

by the first satisfied disjunct in the formula with the unbound variables x andy instantiated by the s and t arguments.

5.3

Compiling Composite Actions

Some automated reasoning method applicable to composite actions is needed
before they become useful in practice. Section 3.3 hinted that direct application of first-order theorem proving techniques does not necessarily result in apractical system. Composite actions are translated into fixpoint logic where
first-order proof methods are not even applicable. An alternative automatedreasoning method is the compilation into constraint logic programs in Chapter 4, which can be extended to the case of composite actions.
The compilation results in a Prolog goal that when evaluated will produce
the actual execution trace of primitive action occurrences where conditionals
have been resolved, non-deterministic choices instantiated, and iteration fixpoints reached. As before, these primitive action occurrences are stored in areified action occurrence arument p. Note that only primitive action occurrences are reified while composite action occurrences are Prolog clauses. The
reified action occurrence argument does not contain composite actions but isintroduced for compatibility with the deductive planning framework. Reified
composite actions is a more complex topic, as discussed in Section 5.4.

5.3.1

The Compilation Function

The first compilation step, the translation from L(ND) into fixpoint logic, wasintroduced above. The second, and final step, is the compilation from fixpoint
logic into constraint logic programs. The compilation is most easily definedrecursively since a composite action may be composed of other composite actions. The compilation will be associated with a function named Comp for the
purpose of conveniently expressing this recursion. The base case of the compilation function, the primitive action occurrence, is defined as the corresponding
Prolog clause:defComp(Occurs(t1 , t2 , a, p)) =occurs(T1,T2,a,P)

Sequences are composed of two composite actions in series, with constraints on
the shared timepoint:

50

Composite Actions

def

Comp(∃t[t1 < t < t2 ∧Trans([t1 , t] A1 ) ∧Trans([t, t2 ] A2 )]) =T1 #< T, T #< T2, Comp(Trans([t1 , t] A1 )), Comp(Trans([t, t2 ] A2 ))Conditionals consist of two complex parts, a condition C and an action A. The
translation of the condition C needs special care. If C evaluates to true, theset of action occurrences should include A, however, we do not want the evaluation of C itself to affect the set of action occurrences. This is accomplishedby minimizing the action occurrences in the variable p through a function circthat removes the unbound tail variable in the corresponding Prolog list variable
P. The result is a new action occurrence variable Pp (a legal Prolog variable
name, unlike P’) where we have assumed complete knowledge about action
occurrences. Using this new, circumscribed, variable when evaluating the condition C prevents the addition of new actions. The implication can then be
written using the Prolog disjunction operator ; as:defComp(Trans([t1 ] C) → Trans([t1 , t2 ] A)) =circ(P,Pp), Comp(Trans([t1 ] ¬C)) ; Comp(Trans([t1 , t2 ] A))
Nondeterministic choices have an existentially quantified variable that is simply
replaced by a Prolog variable in the resulting expression:
defComp(∃x[Trans([t1 , t2 ] A)]) =Comp(Trans([t1 , t2 ] A)) with occurrences of x replaced by X
Loops, with the additional action occurrence argument, are compiled in two
steps. First, the implicit least fixpoint function X is made explicit as a Prolog
predicate x that defines the loop. As with conditional actions, the test C isevaluated with the action occurrence variable P replaced by a circumscribedversion Pp. Secondly, a Prolog goal calls the new predicate to evaluate theactual parameters passed to the function:
Comp(µX(x, y, p)[Trans([x] ¬C) →def∃z[x < z ≤ y ∧Trans([x, z] A) ∧ X(z, y, p)]](t1 , t2 , p)) =a new Prolog predicate:x(X,Y,P) :- circ(P,Pp), Comp(Trans([x] C)) ;X #< Z, Z #=< Y, Comp(Trans([x, z] A)), x(Z,Y,P).
and the goal:x(t1 ,t2 ,P)Finally, since Prolog is not typed, nondeterministic choice variables and quantified variables in test conditions require additional clauses that represent unary
type predicates. These ensure that the variables can only be bound to objectsof the correct type. As before, the special timepoint clause assigns a finite
domain to the timepoint constraint variables.

5.3. Compiling Composite Actions

5.3.2

51

An Example Composite Action

Consider the attach action TAL narrative from Chapter 4 extended with aconverse drop action and a fly action. These primitive actions can be used towrite composite actions for the delivery of crates between locations. E.g., onesuch logistics task is to fly a UAV to fetch crates at a location loc1 and deliver
them to another location loc2 until there are at least two crates there. All of
the different types of composite actions are present in its specification:[0, t] do (if ¬loc(uav1) =ˆ loc1 then fly(uav1, loc1);
choose c (attach(uav1, c);fly(uav1, loc2);drop(uav1, c)))until ∃c1 , c2 [loc(c1 ) =ˆ loc2 ∧ loc(c2 ) =ˆ loc2 ∧ c1 6= c2 ]The composite action is first translated into L(FL):µX(x, y, p)[¬∃c1 , c2 [Holds(x, loc(c1 ), loc2, p) ∧ Holds(x, loc(c2 ), loc2, p) ∧ c1 6= c2 ] →∃z [x < z ≤ y ∧∃t1 [x < t1 < z ∧(¬Holds(x, loc(uav1), loc1, p) →Occurs(x, t1 , fly(uav1, loc1), p)) ∧∃c [∃t2 [t1 < t2 < z ∧Occurs(t1 , t2 , attach(uav1, c), p) ∧∃t3 [t2 < t3 < z ∧Occurs(t2 , t3 , fly(uav1, loc2), p) ∧Occurs(t3 , z, drop(uav1, c), p)]]]] ∧X(z, y, p)]](0, t, p)
The logic program compilation then creates a new Prolog predicate that defines
the least fixpoint loop formula, with additional type and timepoint predicates:
x(X,Y,P) :circ(P,Pp1), crate(C1), crate(C2), holds(X,loc(C1),loc2,Pp1),
holds(X,loc(C2),loc2,Pp1), C1 \== C2 ;timepoint(Z), X #< Z, Z #=< Y,timepoint(T1), X #< T1, T1 #< Z,((circ(P,Pp2), holds(X,loc(uav1),loc1,Pp2)) ;occurs(X,T1,fly(uav1,loc1),P)),crate(C), timepoint(T2), timepoint(T3), T1 #< T2, T2 #< Z,
occurs(T1,T2,attach(uav1,C),P),
T2 #< T3, T3 #< Z,52

Composite Actions

occurs(T2,T3,fly(uav1,loc2),P),
occurs(T3,Z,drop(uav1,C),P),
x(Z,Y,P).
Finally, the Prolog goal consists of calling the new predicate with the actual
parameters:?- x(0,T,P), timepoint_variables(L), labeling([],L).
The timepoint variables predicate collects all the finite domain constraint
variables expressing temporal constraints and the labeling predicate ensures
their consistency (or forces backtracking otherwise).
Evaluating the goal in an initial state where the UAV is already at location
loc1 binds the action occurrence argument P to the following sequence of action
occurrences:
occ(t1 , t2 , attach(uav1, crate1))
occ(t2 , t3 , fly(uav1, loc2))
occ(t3 , t4 , drop(uav1, crate1))
occ(t4 , t5 , fly(uav1, loc1))
occ(t5 , t6 , attach(uav1, crate2))occ(t6 , t7 , fly(uav1, loc2))
occ(t7 , t8 , drop(uav1, crate2))
0 < t1 < t2 < t3 < t4 < t5 < t6 < t7 < t8 ≤ t

5.4

Reified Composite Actions

The composite actions that we have presented are given by an operator andexecuted by the robot. This is similar to how primitive actions were usedin TAL before our deductive planning extensions. Just as reified action occurrences made deductive planning with primitive action occurrences possible, one
would like to use reification or some other scheme to make deductive planningwith composite actions possible. However, since the semantics of composite
actions are expressed in fixpoint logic there is no complete proof procedurethat can be applied in the general case. Moreover, loops and conditionals makeup a Turing complete language, thereby equating the generation of composite
actions with the general problem of program synthesis. These considerations
bodes for both great challenges and great rewards for future research in thisdirection.

Chapter 6

A UAV Logistics
Application
We call the constraint logic programming methodology just described PARADOCS for Planning And Reasoning As DeductiOn with ConstraintS. It has
been integrated with our autonomous unmanned aerial vehicle system and applied to solving logistics problems to test the viability of the method.
The integrated system can use the set of actions in the logistics scenario from
Section 5.3.2 to distribute crates according to a declarative goal specification
by generating a plan that involves repeatedly attaching a crate, flying, andthen dropping it at the intended location. The UAV operator uses a graphicaldrag’n’drop user interface to set up the goal specification for a mission. The
goals are sent to a Prolog program that is compiled from the logistics TAL
narrative. Executing the program corresponds to proving the goal, and a partial
order plan is extracted from the constraint stores that result from the proof.
The operator uses the GUI to choose a linearization, which is compiled into
a sequence of commands that can be executed by the UAV system. The nonocclusion constraints on fluent values are then monitored during the actual
execution to make sure that it proceeds according to the plan. A failure of amonitor condition triggers a plan repair where the current state of execution
is used by PARADOCS to insert recovery actions that will put the execution
back on track and ensure that the goals are satisfied.
This chapter describes the implementation of the above scenario when coupled to the helicopter simulator. We are currently at work building a winch
system with an electro-magnetic hook and trying to solve the vision problems
associated with detecting crates and hovering with sufficient precision over53

54

A UAV Logistics Application

Figure 6.1: A logistics mission in the graphical user interface.
them. These enhancements would make it possible to perform the scenario
using the helicopter hardware.

6.1

Graphical User Interface

The graphical user interface is implemented in Lisp using the Franz Allegro
CL Common Graphics multi platform GUI library [15]. It provides a window
based interface with an aerial overview of the flying area overlayed by icons
representing objects of interest. Setting up a logistics mission simply consistsof dragging crate icons to indicate their intended goal locations. Consider e.g.
the mission set up in Figure 6.1. The task is to deliver three crates froma common store to three different locations. Clicking the “Generate Plan”

6.1. Graphical User Interface

55

button will call on SICStus Prolog 3.12.5 [30] to evaluate the logic program(found in the appendix) on the following goal generated by the interface::- holds(T,loc(crate3),pos(113,-96),P),
holds(T,loc(crate1),pos(82,6),P),
holds(T,loc(crate2),pos(277,12),P),
timepoint_variables(L), labeling([],L).
Iterative deepening on timepoint variable domains would generate a plan withthe smallest consistent temporal network. Such an exhaustive search would
be completed on an Intel Pentium M 1.8 GHz within thirteen minutes. But
the goal-directed search exhibited by PARADOCS is able to find plans in thelogistics scenario without a depth bound. The plans are not guaranteed to
be optimal, but they avoid the complete exploration of the search space oneach depth bound smaller than the one that produces the first plan. With
this approach PARADOCS produces a plan consisting of 12 actions and 15
persistence intervals in a graph containing a total of 22 temporal intervals in
less than a tenth of a second.
The need for a graphical interface was evident even during the development
and experimentation with deductive planning and temporal constraints. The
constraint networks are represented as predicate lists by the constraint solver.
These lists quickly grow unreadably large, prompting some form of visualization
tool for grasping the temporal relations between action intervals and fluent
persistence intervals. The first of two such visualizations in the GUI is aninterval algebra graph that displays the partially specified temporal relations
between intervals. Figure 6.2 shows the solution graph for the above logistics
mission. The interval algebra representation’s support for partial knowledge inthe form of disjunctions makes it impossible to visualize the order in which theactions of the plan will be executed. In fact, at this point the order has not yet
been decided. Still, it is possible to partially order the graph so that intervals
higher up in the display are known to occur before intervals below them.
Even though transitive and reflexive relations are hidden the graph is still
difficult to decipher for all but the tiniest of plans. Instead, the operator clicks
a “Next Linearization” button to apply a backtracking labeling algorithm that
returns all possible linearizations of the partial order plan, one at a time. At
this point visualization is much easier as the order of actions has been decided.
The plan chart in Figure 6.3 shows the first linearization of the above graph.

56

A UAV Logistics Application

Figure 6.2: An interval algebra graph visualization of a partially ordered plan.

6.2

Execution and Monitoring

The GUI provides an interface for an operator of the UAV to the PARADOCS
planning service, which is part of the software system that controls the robot
platform [6]. The software system implements a deliberative/reactive architecture where components use the CORBA framework to call each other’s methods. This enables a highly distributed system in which components can use
different implementation languages and reside on different computers as longas they are connected in a network.
Planned actions are stored in an action queue. They are popped from thequeue during execution and communicated to a Command Executor service
that assumes responsibility for calling the appropriate low-level control functionalities to execute each action. The planned actions are guaranteed to beconsistent with the persistence assumptions that were made during the plan-6.2. Execution and Monitoring

57

Figure 6.3: A plan chart showing one of many possible linearizations of theplan.
ning process, but unexpected things can happen during execution. The plan’s
persistence constraints, in the form of non-occlusion formulas that must holdduring specific time intervals, are therefore placed in a monitor queue in parallell with the action queue. Monitor constraints that are active during aninterval are evaluated by regularly querying the simulator for the values ofthe fluents and making sure that the values are indeed persistent and do notchange.
Assume however, for the sake of example, that the electro-magnet devicelooses hold of crate1 while the UAV is flying towards its destination in the
middle of executing the plan in Figure 6.3. The planning process had alreadyrecorded the assumption that the fluent carrying(uav1,crate1) is persistent during the flight. This is necessary to satisfy the conditions for the action of dropping crate1 at its destination. But when the hold of the crate is lost, the truth
value of the carrying fluent changes to false, which violates said monitoring
formula. At this point the plan is no longer guaranteed to achieve the goal andexecution is halted.
Since PARADOCS can be applied equally well to problems in-between planning and prediction we can use the part of the plan that has not yet been
executed as input for a plan repair process. The following goal is automatically generated and passes the actions that are left to execute as input throughthe action occurrence argument and ensures that they satisfy the previously

58

A UAV Logistics Application

selected linearization using constraints on the timepoint variables::- P = [occ(T1,T2,fly(uav1,pos(82,6))),
occ(T2,T3,drop(uav1,crate1)),occ(T4,T5,fly(uav1,pos(175,-35))),occ(T5,T6,attach(uav1,crate3)),occ(T6,T7,fly(uav1,pos(113,-96))),
occ(T7,T8,drop(uav1,crate3))|Pp],
T1 #< T2, T2 #< T3, T3 #< T4, T4 #< T5,
T5 #< T6, T6 #< T7, T7 #< T8,holds(Tn,loc(crate3),pos(113,-96),P),
holds(Tn,loc(crate1),pos(82,6),P),
timepoint_variables(L), labeling([],L).
The result is, in this case, the insertion of a fly(uav1,pos(153,2)) and an
attach(uav1,crate1) action in front of the rest of the plan. These actions
constitute a recovery by going back to pick up the crate that was accidentally
dropped before continuing with the rest of the plan.

Chapter 7

Related Work
Much of the inspiration to our work comes from other research groups withsimilar approaches. We list here only the most important influences and startwith Shanahan’s abductive Event Calculus planner [33]. It is based on the
Event Calculus, a logical formalism for reasoning about action and change
that, like TAL, uses an explicit time line and an Occurs predicate to link action occurrences to the time line. This makes it suitable for the generation ofpartially ordered plans and, as with PARADOCS, practical planning is accomplished using logic programs. However, plan synthesis is based on abductionof Occurs instead of deduction with reified action occurrences. The use of
abduction results in theoretical elegance, but performing abduction in a logic
program requires an abductive meta-interpreter, which makes the programs
more complex.
The timepoint relations of the abductive Event Calculus planner can only
detect inconsistencies caused by conflicts between action preconditions andaction effects if the order of timepoints involved in the conflict is known. Consistency is guaranteed by adding new timepoint relations in what could be
described as the logical equivalent of the promote/demote strategy from partial order planning algorithms (page 12, [33]). But resolving potential conflicts
through promotion or demotion represents an early commitment to a specificordering, and both orderings must be evaluated in cases where the planning
process backtracks. Our constraint logic programs take full advantage of therepresentational power of disjunctive interval algebra relations. Disjunctive
non-overlap constraints allow the planner to postpone decisions on the ordering of actions, even in the case of a possible conflict, thereby reducing the search
space. We have in fact experimented with weaker constraint solvers similar to

59

60

Related Worksimple temporal networks, but found the added complexity of the implementation that result from the introduction of promotion and demotion to detractfrom the clarity of presentation. Although the use of disjunctive constraints is
associated with an increase in the computational complexity of the constraint
propagation algorithms, the complexity is still overshadowed by the complexityof planning in general.
In a feature comparison, the Event Calculus planner extends our basic planning capabilities with hierarchical planning and a form of knowledge producing
sensing actions that are also based on abduction [34].
Another deductive planning framework is GOLOG [21], which extends the
Situation Calculus with composite actions, including the sequences, conditionals, non-deterministic choices, and loops that we introduced in Chapter 5. The
paradigm is slightly different in that it views the resulting formalism as ahigh-level agent programming language where the programmer supplies a possibly incomplete program specification, and the robot’s task is to execute thespecification while resolving non-determinism that may result from its incompleteness.
The Situation Calculus originated the idea of reified action occurrences
passed around using an extra predicate argument. But its situation terms contain linearly ordered action sequences without explicit temporal information,
which prevents the generation of partially ordered plans. Note however, thatsuch shortcomings can be overcome through various extensions, as is done e.g.
in ConGolog [11]. Both the Situation Calculus and the GOLOG framework
have been extended in a number of other interesting ways, e.g. for planningwith incomplete information about the initial state [9].
While GOLOG uses composite actions to provide a form of search control
through domain dependant knowledge, complex actions are not part of theplanning process in the way that simple actions are. This is no great surprisesince, as we noted in Section 5.4, the resulting system would in fact perform
program synthesis. However, Levesque’s KPLANNER [20] explores an interesting middleground between the direct synthesis of programs with loops and
GOLOG’s execution of non-deterministic loops supplied by a programmer. It
is applicable to problems where it is possible to identify a single fluent, whose
value is unknown or unbound, that is responsible for making the problem unsolvable without the generation of plans containing loops. The method consistsof setting a relatively small upper bound on the value of this fluent, generatinga plan with help from a clever Prolog function that “winds up” action sequences
into loops, and finally testing this plan for a larger bound (since testing will becheaper than generating). Using this method one can generate plans with loops
that are correct up to the testing bound, and, for some classes of problems,

61

provably correct for any value of the unbounded fluent.
Another approach to the use of composite actions in planning is presentedby McIlraith and Fadel [27] who were motivated by the needs of planning for
the use of semantic web services, but also by the increased plan generation efficiency resulting from the possibility of shorter solution plans. They provide acompilation, expressed in terms of the Situation Calculus, of action sequences,conditionals, and loops, into a new set of actions that are not composite. However, due to the requirements enforced on the composite actions to ensure thatthe compilation is possible, only bounded loops with a predetermined maximum number of iterations are considered. Our PARADOCS framework does
not provide a means for the direct use of composite actions in planning, but
our loop semantics, expressed in terms of a fixpoint formula, is not associatedwith any preset bounds.
The Fluent Calculus serves as the formal basis for FLUX [37], another logic
programming methodology that supports deductive planning with linear plans.
It was mentioned earlier as the source of the Prolog list membership function
implementation used for adding reified action occurrence terms to a list. In
FLUX the same predicate is used for a different purpose as the basic mechanismof representing states as sets of fluents. Constraint handling rules are also usedin FLUX, but again for different purposes than ours. While we utilize CHR
for detecting and resolving potential conflicts between action effects and fluent
persistency, in FLUX they enable the planning and reasoning with incomplete
information and also reasoning about knowledge and knowledge updates ascaused by sensing actions. Although the form of the expressions over whichsuch reasoning is allowed is limited, the limitations ensure that the allowed
reasoning is computationally efficient.
Our final example of logic programming based planning is answer set planning, as described e.g. by Lifschitz [23]. Answer set programming is purely
declarative, and thus avoids some of the problems inherent in Prolog, such as
the possibility of the evaluation becoming stuck in an infinite loop. This property makes it easier to add temporal constraints and state constraints on theanswer generation. Lifschitz proposes that its use of both classical negationand negation as failure makes it suitable for specifying the effects of actions
and the non-monotonic behaviour of the persistence of fluents that they affect.
In addition, Son, Baral, and McIlraith [35] show how answer set programming can be extended with sequences, conditionals, non-deterministic choice,and loops, to construct an alternative GOLOG interpreter. This can be used,in the same way as any Prolog GOLOG interpreter, to write non-deterministic
programs that, in effect, express domain-specific control knowledge restricting
the search for solution plans.

62

Related Work

However, the evaluation mechanism of answer set programs includes instantiating the problem into a finite number of propositions, and is thus only
applicable to finite theories with a fixed upper time bound. While such a“propositional” approach, also used in the planning as satisfiability paradigm,
may be simple and robust, it can suffer from an exponential increase in thesize of the representation of the problem. It also lacks the goal-directedness of
Prolog’s evaluation mechanism, based on theorem proving, that seems to us tobe a desireable property that will be absolutely necessary as the complexity ofproblems a robot attempts to solve increases, and as the number of different
means it has available to apply to the problems grows.
An even stronger programming language focus is displayed by agent programming languages such as 3APL [14]. The concept of a goal is considered
to be procedural rather than declarative, and actions are described as state
updates that modify an agent’s beliefs, rather than being defined by sets ofaxioms. While 3APL provides a formal semantics, it is an operational semantics distinct from the programming language itself. Although the proceduralview of goals might seem restrictive, from the point of view of planning, it issurprisingly close to e.g. GOLOG’s programs. In fact, it is possible to embed
ConGolog into 3APL [13].
Another system with a focus on planning, and with many features in common with PARADOCS, is Allen’s temporal planner [2]. It expresses temporal
information using the interval temporal logic that axiomatizes the interval algebra and extends it with atomic time periods that behave like timepoints
and represents actions by reified events. Allen also stresses the importanceof viewing different types of reasoning as inference in a common representation, although, the actual plan synthesis is cast as an algorithm that closely
approximates a proof procedure.
A different view is endorsed in planners that utilize special purpose planningalgorithms. TALplanner [7] is one such planner that is especially close to oursin that it makes use of the same Temporal Action Logic. However, the purposeof TAL in TALplanner is as a formal semantics of actions, goals, and plans.
Employing Temporal Action Logic as a formal semantics for the actual planning
process, and using it directly for plan synthesis, prompted the extensions andwork described in this thesis.
Karlsson proceeds with a more theoretical emphasis when he presents his
Narrative Logic, based on TAL but with its own extensions for reified action
occurrences [16]. Karlsson formulates the planning task in Narrative Logic but,
although he provides a translation from Narrative Logic into classical logic, theresult is a second-order theory that is not directly amenable to automated theorem proving. In contrast, our translation of TAL with reified action occurrences

63

into logic programs makes the logic directly applicable in practice.
Both Karlsson’s work and ours extend TAL, which itself originates in Sandewall’s Features and Fluents framework [32]. In fact, Sandewall himself provides a formulation of composite actions, including sequences, conditionals,
and loops, whose macro-language syntax is almost identical to ours. However,
the translation of loops differs significantly. Sandewall uses a first-order definition involving special signal features, which are introduced only to keep trackof the looping behaviour. This results in a specification that is rather complex,
whereas our formulation in terms of a fixpoint formula is significantly simpler
while succinctly capturing the looping property.
Furthermore, we extend Sandewall’s set of composite actions with nondeterministic choice, which we found necessary for composite actions to beof practical use, and we make such use possible through the provision of ourcompilation into logic programs.

64

Related Work

Chapter 8

Discussion
Although Temporal Action Logic has long served as a formal basis for some of
our work in cognitive robotics, we set out to use TAL for deductive planning.
This effort necessitated some theoretical additions to the logic but has also resulted in a compilation process that extends the translation from the high-level
language L(ND) to constraint logic programs that are efficiently executed forpractical planning. The persistence constraints that are part of the generated
plans can be used for execution monitoring purposes and the integration ofplan synthesis and reasoning about plans is put to use in the failure recovery
process. The entire set up is integrated with our UAV system and can be usedthrough a graphical user interface with drag’n’drop mission planning to executelogistics missions in our helicopter simulator that adds a winch and crates toour fully operational UAV research platform.
The explicit time representation of TAL exposes qualitative and quantitative temporal primitives that are particularly amenable to reasoning using
temporal constraint formalisms. The method can be made to work with a variety of constraint formalisms for both qualitative and quantitative constraints,
such as simple timepoint constraints, interval algebra, or general temporalconstraint networks. But the combination of constraint handling rules anddisjunctive temporal constraints is particularly suited to the TAL formalism.
This, together with the occlusion concept, enables a novel solution to potential
action/persistence conflict threats where promotion/demotion is postponed,
thereby removing search space choice points and resulting in flexible solutionplans.

65

66

8.1

Discussion

Future Research

While compiling narratives into logic programs that can be used for deductiveplanning works very well, the technique is ultimately limited. As stated in the
introduction Section 1.1, our two main motivations for planning deductively
are uniformity and expressiveness. But the expressivity of logic programs are
inherently limited, and each attempt to circumvent specific limitations using
additional special purpose techniques will result in decreasing uniformity. For
these reasons we believe a move towards a more direct use of theorem proving
in the first-order base logic of TAL to be important.
A move from logic programming towards more general theorem proving will
surely lead to inefficiency and scalability problems. The resulting system might
only be able to reason with relatively small problem instances and complexity
might prevent it from scaling up to problem instances of a larger size that could
have been solved by a less expressive system. Though, the class of problems towhich the system is applicable would be larger. And when that class expands
to encompass the generation of plans with loops or recursion, as discussed in
Section 5.4, the rules of the game suddenly change. Consider e.g. a logistics
scenario where the number of crates to be delivered is unspecified. Any solution
plan will have to contain some form of looping or recursion behaviour that
iterates over the crates until the goal has been satisfied. Plans of this highly
expressive sort can probably be small and compact. Moreover, the plan isof constant size, regardless of the size of the logistics problem instance that
it is later applied to. Finally, the solution simultaneously solves all problem
instantiations with any number of crates. In contrast, a less expressive planner
would not be applicable to a logistics problem where it is unknown what crates
exists. It would exhibit an often exponential, but at least linear, increase inplanning time and a linear increase in solution length as the size of the problem
instance grows. Finally, it would require more planning and the generation of anew plan every time a new problem instance with a different number of crates
needs to be solved.
The problem of generating plans with loops or recursion is a very difficult
problem to which deductive planning with theorem proving techniques has been
applied with some success [26, 3, 4]. In addition to the “plans as programs”
paradigm, deductive planning with a highly expressive representation is potentially applicable to a large number of other interesting problems. Two of
the most important are planning in the context of incomplete information andreasoning about knowledge and knowledge-producing sensing actions. Both arepossible continuations of the work in this thesis.

8.2. Conclusions

8.2

67

Conclusions

Nilsson [29] argues for a distinction between general intelligent systems and specialized systems that exhibit greater than human performance in a relatively
narrow area of expertise. A logical framework for reasoning and planning withactions is, by design, aimed towards generality rather than performance whencompared with a special purpose planner. This thesis presents a methodology for practical deductive planning in TAL that is a step towards a uniform
way of tackling increasing complexity. Moving towards increasingly intelligent
autonomous systems means requring less help from humans who predict anddecide what tools need to be applied in solving a given task. At the sametime, the increasing diversity and challenge of the tasks themselves require
the application of flexible and powerful reasoning methods. By reformulating
special-purpose algorithms as proof search in a shared representational formalism, one removes the need to decide in advance what algorithms are needed
to solve future tasks. Through the use of highly expressive logical formalisms
and automated theorem proving technology one opens the possibility of attacking a great many different and complex reasoning problems in a uniform way.
Although this unifying approach might not have been the way of the (recent)past, the growing challenges of artificial intelligence applications is increasing
its appeal as the way of the future.

68

Discussion

Appendix A

The Logistics Scenario
Prolog CodeThis appendix contains the UAV logistics scenario constraint logic program
encoding that has been integrated with the autonomous helicopter system andwas used for the planning examples in Chapter 6. Readers interested in runningthe program can also access this code in electronic form at this thesis’ website:
http://www.martinmagnusson.com/paradocs/thesis/.
Three additional comments will assist understanding of the code. Firstly,
the persistence clauses have a potential problem with infinite looping given thedepth-first search strategy of Prolog. A fluent is true at a timepoint if it is trueat an earlier timepoint and is not occluded during the interval in between. It istrue at the earlier timepoint if it is true at an even earlier timepoint, and so on.
The looping is correct but unwanted behaviour. But the observation that if afluent is persistent over two intervals that meet, then it must be persistent overthe union of the intervals, provides the key to a simple solution. Without loss ofgenerality we prohibit two consecutive persistence intervals using an additional
constraint that appears in the code below with the comment “Consecutive
persistence constraint”.
Secondly, although there is only one UAV in our scenario there are few
restrictions on the occurrence times of actions, which can lead to modellingproblems related to concurrency. The UAV magnetic hook can be seen as alimited resource that can not attach several crates at once. However, modelling
this using a fluent precondition free that is set to false when executing attachdoes not prevent two concurrent attach at the exact same time. Actions canonly have effects in the future, so one attach can not prevent another attach
69

70

The Logistics Scenario Prolog Codefrom executing simultaneously by setting free to false at the next timepoint.
Gustafsson [12] suggests a way of solving this problem using TAL narratives
where actions do not have direct effects on fluents, but rather activate special
influence fluents. Dependency constraints are then used to express influencelaws that govern the effects of influences on the environment, and thereby theindirect effects of actions. Concurrent planning in TAL, using an explicit timeline and powerful temporal constraints solvers, holds great promise but clearlyneeds more investigation. We avoid the issue for now and instead add two concurrency constraints even though they are not part of the translation specified
in Chapter 4. Specifically, the constraints with the comment “Concurrency
constraints” prohibit the UAV from carry several crates and from flying toseveral places concurrently.
Thirdly, and finally, at the same time that non-overlap constraints are added
to the finite domain constraint store, they are stored in the CHR store using a
constraint named ia. The final group of clauses, which appear below the comment “Backup store”, are then used to create a copy of the CHR constraint
store before the labeling of timepoint variables that determines if the interval
algebra network is consistent. This prevents the labeling process from instantiating and unifying timepoint variables in the network copy while searchingfor a consistent linearization of the original, thereby preserving all of the partialness of the ordering of action occurrences. The final interval algebra graphis then easily read from the ia constraint in the constraint store copy, and it
is guaranteed to be consistent since the original went through a labeling.
:- use_module(library(chr)).
:- use_module(library(clpfd)).
:- use_module(library(charsio)).
% CHR definitions:handler tal.
constraints not_occlude/3, circ_occurs/3, tp/1, ia/3.
% Occurs definition:
occurs(T1,T2,A,P) :member(occ(T1,T2,A),P), circ_occurs(T1,T2,A).
member(A,[A|Pp]).
member(A,P) :nonvar(P), P = [A1|P1], A \== A1, member(A,P1).
% Interval relations:
not_overlap(Xs,Xe,Ys,Ye) :-71

Xe #=< Ys #\/ Xs #>= Ye,ia(Xs-Xe,[<,m,mi,>],Ys-Ye).
% Type clauses:
timepoint(T) :- domain([T],0,100), tp(T).
uav(uav1).
crate(crate1).
crate(crate2).
crate(crate3).
% Persistence formulas:
holds(T2,loc(X),V,P) :timepoint(T1), timepoint(T2), T1 #< T2,
not_occlude(T1,T2,loc(X)),
holds(T1,loc(X),V,P).
holds(T2,carrying(U,C),V,P) :timepoint(T1), timepoint(T2), T1 #< T2,
not_occlude(T1,T2,carrying(U,C)),
holds(T1,carrying(U,C),V,P).
% Consecutive persistence constraint:
not_occlude(T1,T,F), not_occlude(T,T2,F) ==> fail.
% Initial state (example):holds(0,loc(uav1),pos(237,-23),P).
holds(0,loc(crate1),pos(202,0),P).
holds(0,loc(crate2),pos(210,-10),P).
holds(0,loc(crate3),pos(200,-13),P).
% Action specifications:holds(T2,loc(U),L,P) :uav(U), timepoint(T1), timepoint(T2), T1 #< T2,
occurs(T1,T2,fly(U,L),P).
not_occlude(T1,T2,loc(U)),
circ_occurs(T3,T4,fly(U,L)) ==>not_overlap(T1,T2,T3,T4).
holds(T2,carrying(U,C),true,P) :uav(U), crate(C), timepoint(T1), timepoint(T2), T1 #< T2,
occurs(T1,T2,attach(U,C),P),72

The Logistics Scenario Prolog Codeholds(T1,loc(C),L,P),
holds(T1,loc(U),L,P),
not_occlude(T1,T2,loc(U)).
not_occlude(T1,T2,carrying(U,C)),
circ_occurs(T3,T4,attach(U,C)) ==>not_overlap(T1,T2,T3,T4).
not_occlude(T1,T2,loc(C)),
circ_occurs(T3,T4,attach(U,C)) ==>not_overlap(T1,T2,T3,T4).
holds(T2,loc(C),L,P) :uav(U), crate(C), timepoint(T1), timepoint(T2), T1 #< T2,
occurs(T1,T2,drop(U,C),P),
holds(T1,carrying(U,C),true,P),
holds(T1,loc(U),L,P),
not_occlude(T1,T2,loc(U)).
not_occlude(T1,T2,carrying(U,C)),
circ_occurs(T3,T4,drop(U,C)) ==>not_overlap(T1,T2,T3,T4).
not_occlude(T1,T2,loc(C)),
circ_occurs(T3,T4,drop(U,C)) ==>not_overlap(T1,T2,T3,T4).
% Concurrency constraints:
not_occlude(T1,T2,carrying(U,C1)),
not_occlude(T3,T4,carrying(U,C2)) ==>not_overlap(T1,T2,T3,T4).
circ_occurs(T1,T2,fly(U,L1)),
circ_occurs(T3,T4,fly(U,L2)) ==>not_overlap(T1,T2,T3,T4).
% Remove redundant constraints:
not_occlude(T1,T2,F) \ not_occlude(T1,T2,F) <=> true.
circ_occurs(T1,T2,A) \ circ_occurs(T1,T2,A) <=> true.
tp(X) \ tp(X) <=> true.
tp(X) <=> ground(X) | true.
% Find variables to label:
timepoint_variables(L) :findall_constraints(tp(_),L1),

73

extract_variable(L1,L).
extract_variable([],[]).
extract_variable([tp(T)#_|L1],[T|L2]) :extract_variable(L1,L2).
% Backup store:
copy_constraints(C) :findall_constraints(_,L1),
extract_constraint(L1,L),
format_to_chars(’~w’,[L],C).
extract_constraint([],[]).
extract_constraint([C#_|L1],[C|L2]) :extract_constraint(L1,L2).

74

The Logistics Scenario Prolog Code

Appendix B

ProofsThis appendix collects proofs of some theorems used in the thesis.

B.1

Interval Persistence Formula

The interval persistence formula relates regular, single timepoint, occlusion
with the new interval occlusion.
Theorem∀t [¬Occlude(t + 1, f ) → ∀v [Holds(t, f, v) ↔ Holds(t + 1, f, v)]] ∧∀t1 , t2 , f [Occlude(t1 , t2 , f ) ↔ ∃t [t1 < t ≤ t2 ∧ Occlude(t, f )]] →∀t1 , t2 , f [¬Occlude(t1 , t2 , f ) →∀t [t1 < t ≤ t2 → ∀v [Holds(t − 1, f, v) ↔ Holds(t, f, v)]]]
Proof
Given ¬Occlude(t1 , t2 , f ) we know, by the definition of interval occlusion above,that there does not exist a timepoint t during the interval (t1 , t2 ] at which
Occlude(t, f ) holds, i.e., ¬Occlude(t, f ) must hold for all timepoints in theinterval. The persistence formula then forces the fluent to retain its value fromthe previous timepoint, which is specified in the above theorem by stating thatthe Holds predicate retains its truth value for all possible fluent values v. We
formalize this reasoning in a deductive proof below.
1∀t [¬Occlude(t + 1, f ) → ∀v [Holds(t, f, v) ↔ Holds(t + 1, f, v)]]

P

2
3

∀t1 , t2 , f [Occlude(t1 , t2 , f ) ↔ ∃t [t1 < t ≤ t2 ∧ Occlude(t, f )]]¬Occlude(t1 , t2 , f ) → ¬∃t [t1 < t ≤ t2 ∧ Occlude(t, f )]

P
2

75

76

Proofs

4
5
6
7
8
9
10
11
12
13

¬Occlude(t1 , t2 , f )¬∃t [t1 < t ≤ t2 ∧ Occlude(t, f )]∀t [t1 < t ≤ t2 → ¬Occlude(t, f )]t1 < t ≤ t2 → ¬Occlude(t, f )t1 < t ≤ t2
¬Occlude(t, f )¬Occlude((t − 1) + 1, f )¬Occlude((t − 1) + 1, f ) →∀v [Holds(t − 1, f, v) ↔ Holds((t − 1) + 1, f, v)]∀v [Holds(t − 1, f, v) ↔ Holds((t − 1) + 1, f, v)]∀v [Holds(t − 1, f, v) ↔ Holds(t, f, v)]

1
10, 1112

14∀t [t1 < t ≤ t2 → ∀v [Holds(t − 1, f, v) ↔ Holds(t, f, v)]]

8 − 1315 ∀t1 , t2 , f [¬Occlude(t1 , t2 , f ) →∀t [t1 < t ≤ t2 → Holds(t − 1, f ) ↔ Holds(t, f )]]4 − 14

B.2

H
3, 4
5
6
H
7, 8
9

Interval End-point Equivalence

The following proof validates the useful property of interval occlusion that afluent that is known not to be occluded during an interval will have the samevalue at both end-points of that interval, regardless of the number of timepoints
inbetween.
Theorem∀t1 , t2 , f [¬Occlude(t1 , t2 , f ) →∀t [t1 < t ≤ t2 → ∀v [Holds(t − 1, f, v) ↔ Holds(t, f, v)]]] ∧∀t1 , t2 , f [Occlude(t1 , t2 , f ) ↔ ∃t [t1 < t ≤ t2 ∧ Occlude(t, f )]] →∀t1 , t2 , f [¬Occlude(t1 , t2 , f ) → ∀v [Holds(t1 , f, v) ↔ Holds(t2 , f, v)]]
Proof
The proof is by induction over the length of occlusion intervals. The base caseconsists of intervals of length 1. Such intervals are already covered by the
sub-formula ∀v [Holds(t − 1, f, v) ↔ Holds(t, f, v)] in the interval persistence
formula above, which we make use of in the deduction below.
16 ∀t1 , t2 , f [¬Occlude(t1 , t2 , f ) →∀t [t1 < t ≤ t2 → ∀v [Holds(t − 1, f, v) ↔ Holds(t, f, v)]]]P

B.2. Interval End-point Equivalence

17
18
19
20
21
22
23

77

¬Occlude(t1 , t2 , f )H∀t [t1 < t ≤ t2 → ∀v [Holds(t − 1, f, v) ↔ Holds(t, f, v)]]
16, 17t2 = t1 + 1
the interval has length 1∀t [t1 < t ≤ t1 + 1 → ∀v [Holds(t − 1, f, v) ↔ Holds(t, f, v)]]
18, 19t 1 < t1 + 1 ≤ t 1 + 1 →∀v [Holds((t1 + 1) − 1, f, v) ↔ Holds(t1 + 1, f, v)]
20∀v [Holds(t1 , f, v) ↔ Holds(t1 + 1, f, v)]
F, 21∀v [Holds(t1 , f, v) ↔ Holds(t2 , f, v)]
19, 2224 ∀t1 , t2 , f [¬Occlude(t1 , t2 , f ) →∀v [Holds(t1 , f, v) ↔ Holds(t2 , f, v)]]

17 − 23

In the inductive case we assume that the theorem holds for intervals of lengthn and show that it holds for intervals of length n + 1. First note that, by thedefinition of interval occlusion, if the fluent is interval occluded over an interval(t, t + n + 1], of length n + 1, then it must also be interval occluded over the
sub-intervals (t, t + n] and (t + n, t + n + 1], of length n and 1 respectively.
Since we assumed that the theorem holds for intervals of length n, the fluent
will have the same value at t and t + n. As with the interval of length 1 in thebase case, the interval persistence formula forces the fluent to retain its value
between t + n and t + n + 1. Taken together these two conditions establish
the conclusion that the fluent will necessarily have the same value at both endpoints of intervals of length n + 1. This is formalized, somewhat cumbersomely,in the deduction below.
25 ∀t1 , t2 , f [¬Occlude(t1 , t2 , f ) →∀t [t1 < t ≤ t2 → ∀v [Holds(t − 1, f, v) ↔ Holds(t, f, v)]]]
P
26 ∀t1 , t2 , f [Occlude(t1 , t2 , f ) ↔ ∃t [t1 < t ≤ t2 ∧ Occlude(t, f )]]P¬Occlude(t1 , t2 , f )H
27
28
t2 = t1 + n + 1
the interval has length n + 1
29¬Occlude(t1 , t2 , f ) → ¬∃t [t1 < t ≤ t2 ∧ Occlude(t, f )]2630¬∃t [t1 < t ≤ t2 ∧ Occlude(t, f )]27, 2931∀t [t1 < t ≤ t2 → ¬Occlude(t, f )]30
t1 < t ≤ t1 + n
H
32
33
t1 < t ≤ t2 − 1
28, 3234
t1 < t ≤ t2
33, F35
¬Occlude(t, f )31, 3436

t1 < t ≤ t1 + n → ¬Occlude(t, f )32 − 35

78

Proofs

37
38
39
40
41
42
43
44

∀t [t1 < t ≤ t1 + n → ¬Occlude(t, f )]¬∃t [t1 < t ≤ t1 + n ∧ Occlude(t, f )]¬Occlude(t1 , t1 + n, f )∀v [Holds(t1 , f, v) ↔ Holds(t1 + n, f, v)]
t1 + n < t ≤ t1 + n + 1
t1 < t ≤ t1 + n + 1
t1 < t ≤ t2
¬Occlude(t, f )

45
46
47
48
49

t1 + n < t ≤ t1 + n + 1 → ¬Occlude(t, f )∀t [t1 + n < t ≤ t1 + n + 1 → ¬Occlude(t, f )]¬∃t [t1 + n < t ≤ t1 + n + 1 ∧ Occlude(t, f )]¬Occlude(t1 + n, t1 + n + 1, f )∀t [t1 + n < t ≤ t1 + n + 1 →∀v [Holds(t − 1, f, v) ↔ Holds(t, f, v)]]
t1 + n < t1 + n + 1 ≤ t1 + n + 1∀v [Holds(t1 + n, f, v) ↔ Holds(t1 + n + 1, f, v)]∀v [Holds(t1 , f, v) ↔ Holds(t2 , f, v)]

25, 48
F
49, 5028, 40, 51

53 ∀t1 , t2 , f [¬Occlude(t1 , t2 , f ) →∀v [Holds(t1 , f, v) ↔ Holds(t2 , f, v)]]

27 − 52

50
51
52

36
37
26, 3839, inductive assumption
H41, F
28, 4231, 4341 − 4445
46
26, 47

By the principle of mathematical induction, the theorem holds for intervals of
any length.

B.3

Point-interval Rewrite

This particular equivalence-preserving rewrite is used in the compilation of a
TAL theory to replace timepoint occlusion formulas with equivalent formulas
expressed using interval occlusion.
Theorem∀t [P (t) → Q(t)] ↔
∀t1 , t2 [∃t [t1 < t ≤ t2 ∧ P (t)] → ∃t [t1 < t ≤ t2 ∧ Q(t)]]Proof
We start with the ⇒ direction and assume that the left hand side holds. Assume
further that there is some t in the interval (t1 , t2 ] for which P holds, i.e.,B.3. Point-interval Rewrite

79∃t [t1 < t ≤ t2 ∧ P (t)]. Apply the assumed implication P (t) → Q(t) to this t
to show the existence of a timepoint in the interval (t1 , t2 ] for which Q holds,
i.e., ∃t [t1 < t ≤ t2 ∧ Q(t)]. For the ⇐ direction, assume that the right handside holds. Assume further that P (t0 ) holds, for an arbitrary timepoint t0 .
Instantiate the universally quantified t1 and t2 , in the right hand side of thetheorem, to t0 − 1 and t0 respectively. Since t0 is in the interval (t0 − 1, t0 ], andwe assumed P (t0 ), we have ∃t [t0 − 1 < t ≤ t0 ∧ P (t)] and conclude ∃t [t0 − 1 <t ≤ t0 ∧ Q(t)]. The narrow interval permits only one value for the existentiallyquantified timepoint t, namely t0 , and we thus have Q(t0 ). Since t0 was arbitrary,
we conclude that ∀t [P (t) → Q(t)]. The argument is restated formally below.
54
55
56
57
58
59
60

∀t [P (t) → Q(t)]∃t [t1 < t ≤ t2 ∧ P (t)]t1 < t ≤ t2 ∧ P (t)P (t) → Q(t)Q(t)
t1 < t ≤ t2 ∧ Q(t)∃t [t1 < t ≤ t2 ∧ Q(t)]61∃t [t1 < t ≤ t2 ∧ Q(t)]

H
H
H
54
56, 5756, 5859
55, 56 − 60

62

∀t1 , t2 [∃t [t1 < t ≤ t2 ∧ P (t)] → ∃t [t1 < t ≤ t2 ∧ Q(t)]]55 − 61

63
64
65
66
67
68
69
70
71

∀t1 , t2 [∃t [t1 < t ≤ t2 ∧ P (t)] → ∃t [t1 < t ≤ t2 ∧ Q(t)]]P (t0 )∃t [t0 − 1 < t ≤ t0 ∧ P (t)] → ∃t [t0 − 1 < t ≤ t0 ∧ Q(t)]t0 − 1 < t0 ≤ t0 ∧ P (t0 )∃t [t0 − 1 < t ≤ t0 ∧ P (t)]∃t [t0 − 1 < t ≤ t0 ∧ Q(t)]t0 − 1 < t ≤ t0 ∧ Q(t)t = t0Q(t0 )

H
H
63
F, 64
66
65, 67
H69, F
69, 7072
73

Q(t0 )∀t [P (t) → Q(t)]74 ∀t [P (t) → Q(t)] ↔
∀t1 , t2 [∃t [t1 < t ≤ t2 ∧ P (t)] → ∃t [t1 < t ≤ t2 ∧ Q(t)]]68, 69 − 71
64 − 72
54 − 62, 63 − 73

80

ProofsB.4

Shared Timepoint Overlap EquivalenceThis proof relates a formula asserting the existence of a timepoint that is shared
between two intervals, and a simpler timepoint relation that indicates interval
overlap.
Theorem∃t [t1 < t ≤ t2 ∧ t3 < t ≤ t4 ] ↔ t2 > t3 ∧ t1 < t4
Proof
Negating both hand sides provides an alternative formulation of the theorem
in terms of non-overlap:¬∃t [t1 < t ≤ t2 ∧ t3 < t ≤ t4 ] ↔ t2 < t3 ∨ t2 = t3 ∨ t1 = t4 ∨ t1 > t4
Of Allen’s 13 primitive interval relations [1], only the four cases displayed in
Figure B.1 below share no point in common between the two intervals (t1 , t2 ]and (t3 , t4 ], as required by the left hand side of the theorem. As can be seen byinspection, these cases correspond exactly to the disjuncts on the right handside of the theorem.

t1

t1

t2
t3

t4

t2
t3

t1
t4

t3

t2

t4

t1
t3

t2

t4

Figure B.1: The four primitive interval relations where the two intervals shareno common timepoint.
An alternative, formal deductive, proof is provided below.
75
76
77
78
79
80
81

∃t [t1 < t ≤ t2 ∧ t3 < t ≤ t4 ]t1 < t ≤ t2 ∧ t3 < t ≤ t4
t3 < t ∧ t ≤ t2
t 2 > t3
t1 < t ∧ t ≤ t4
t 1 < t4
t 2 > t3 ∧ t 1 < t482

t 2 > t3 ∧ t 1 < t4

H
H
76
77, F
76
79, F
78, 8075, 76 − 81

B.4. Shared Timepoint Overlap Equivalence

81

83
84
85
86
87
88

t 2 > t3 ∧ t 1 < t4t 4 ≤ t 2 ∨ t 4 > t2
t4 ≤ t2
t 1 < t4 ≤ t 2
t 3 < t4 ≤ t 4∃t [t1 < t ≤ t2 ∧ t3 < t ≤ t4 ]HFH83, 85t3 and t4 are endpoints of an interval
86, 87

89
90
91
92
93

t 4 > t2
t 1 < t2 ≤ t 2
t 3 < t2 < t4
t 3 < t2 ≤ t 4∃t [t1 < t ≤ t2 ∧ t3 < t ≤ t4 ]H
t1 and t2 are endpoints of an interval
83, 8991, F
90, 9294∃t [t1 < t ≤ t2 ∧ t3 < t ≤ t4 ]95 ∃t [t1 < t ≤ t2 ∧ t3 < t ≤ t4 ] ↔ t2 > t3 ∧ t1 < t4

84, 85 − 88, 89 − 93
75 − 82, 83 − 94

Bibliography[1] James F. Allen. Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11):832–843, 1983.
[2] James F. Allen. Planning as temporal reasoning. In James F. Allen,
Richard Fikes, and Erik Sandewall, editors, Principles of Knowledge Representation and Reasoning (KR’91), pages 3–14. Morgan Kaufmann, San
Mateo, California, 1991.
[3] Stephen Cresswell, Alan Smaill, and Julian Richardson. Deductive synthesis of recursive plans in linear logic. In Proceedings of the 5th European
Conference on Planning (ECP’99), pages 252–264, London, UK, 2000.
Springer-Verlag.
[4] Lucas Dixon, Alan Smaill, and Alan Bundy. Planning as deductive synthesis in intuitionistic linear logic. Technical report, The University of
Edinburgh Shool of informatics, 2006. http://homepages.inf.ed.ac.
uk/ldixon/papers/infrep-06-planill.pdf.
[5] Patrick Doherty. PMON+ : a fluent logic for action and change, formal
specification, version 1.0. Technical Report LiTH-IDA-R-96-33, Department of Computer and Information Science, Linköping University, 1996.
http://www.ida.liu.se/publications/techrep/96/tr96.html.
[6] Patrick Doherty, Patrik Haslum, Fredrik Heintz, Torsten Merz, Per Nyblom, Tommy Persson, and Björn Wingman. A distributed architecture
for autonomous unmanned aerial vehicle experimentation. In Proceedingsof the 7th International Symposium on Distributed Autonomous Robotic
Systems, 2004.
[7] Patrick Doherty and Jonas Kvarnström. TALplanner: A temporal logic
based planner. AI Magazine, 22(3):95–102, 2001.
82

BIBLIOGRAPHY

83[8] Patrick Doherty and Jonas Kvarnström. Handbook of Knowledge Representation, chapter 18. Elsevier, 2007. To appear.
[9] Alberto Finzi, Fiora Pirri, and Ray Reiter. Open world planning in thesituation calculus. In Proceedings of the 7th Conference on Artificial Intelligence (AAAI’00) and of the 12th Conference on Innovative Applicationsof Artificial Intelligence (IAAI’00), pages 754–760, Menlo Park, CA, July
30– 3 2000. AAAI Press.
[10] Thom Frühwirth. Theory and practice of constraint handling rules. Journal of Logic Programming, Special Issue on Constraint Logic Programming,
37(1–3):95–138, October 1998.
[11] Giuseppe De Giacomo, Yves Lesperance, and Hector J. Levesque. Congolog, a concurrent programming language based on the situation calculus.
Artificial Intelligence, 121(1-2):109–169, 2000.
[12] Joakim Gustafsson. Extending Temporal Action Logic.
Linköping University, 2001. Dissertation No. 689.

PhD thesis,[13] Koen Hindriks, Yves Lespérance, and Hector Levesque. An embeddingof ConGolog in 3APL. Technical Report UU-CS-2000-13, Department ofComputer Science, University Utrecht, 2000.
[14] Koen V. Hindriks, Frank S. De Boer, Wiebe Van der Hoek, and JohnJules Ch. Meyer. Agent programming in 3APL. Autonomous Agents andMulti-Agent Systems, 2(4):357–401, 1999.
[15] Franz Inc. Graphical user interface tools. http://www.franz.com/
products/gui_tools/. Visited November 2006.
[16] Lars Karlsson. Anything can happen: On narratives and hypotheticalreasoning. In Proceedings of the Sixth International Conference on the
Principles of Knowledge Representation and Reasoning (KR’98), pages
36–47, 1998.
[17] Lars Karlsson. Actions, Interactions and Narratives.
Linköping University, 1999. Dissertation No. 593.

PhD thesis,[18] Jonas Kvarnström. VITAL: Visualization and implementation of temporal
action logics. http://www.ida.liu.se/~jonkv/vital/. Visited January
2007.
[19] Jonas Kvarnström. TALplanner and Other Extensions to Temporal Action
Logic. PhD thesis, Linköping University, 2005. Dissertation No. 937.

84

BIBLIOGRAPHY[20] Hector J. Levesque. Planning with loops. In Proceedings of the NineteenthInternational Joint Conference on Artificial Intelligence (IJCAI’05), pages
509–515, 2005.
[21] Hector J. Levesque, Raymond Reiter, Yves Lesperance, Fangzhen Lin, andRichard B. Scherl. GOLOG: A logic programming language for dynamic
domains. Journal of Logic Programming, 31(1-3):59–83, 1997.
[22] Vladimir Lifschitz. Circumscription. In Handbook of Artificial Intelligenceand Logic Programming, volume 3, pages 297 – 352. Oxford University
Press, 1991.
[23] Vladimir Lifschitz. Answer set planning. In Proceedings of the 1999 International Conference on Logic Programming, pages 23–37, 1999.
[24] Martin Magnusson and Patrick Doherty. Deductive planning with temporal constraints using TAL. In Proceedings of the International Symposium on Practical Cognitive Agents and Robots (PCAR’06), pages 141–
152, 2006.
[25] Martin Magnusson and Patrick Doherty. Deductive planning withtemporal constraints.
In Eyal Amir, Vladimir Lifschitz, and Rob
Miller, editors, Logical Formalizations of Commonsense Reasoning: Papers from 2007 AAAI Spring Symposium. AAAI Press, 2007. Technical Report SS-07-05 http://www.ucl.ac.uk/commonsense07/papers/
magnusson-and-doherty.pdf.
[26] Zohar Manna and Richard J. Waldinger. How to clear a block: A theoryof plans. Journal of Automated Reasoning, 3(4):343–377, 1987.
[27] Sheila McIlraith and Ronald Fadel. Planning with complex actions. In
Proceedings of the Ninth International Workshop on Non-Monotonic Reasoning (NMR’02), pages 356–364, Toulouse, France, April 19-21 2002.
[28] Itay Meiri. Combining qualitative and quantitative constraints in temporalreasoning. In Proceedings of the Ninth National Conference on Artificial
Intelligence, pages 260–267, 1991.
[29] Nils J. Nilsson. Eye on the prize. AI Magazine, 16(2):9–17, 1995.
[30] Swedish Institute of Computer Science SICS AB. SICStus prolog homepage. http://www.sics.se/sicstus/. Visited November 2006.
[31] Francis Jeffry Pelletier. A brief history of natural deduction. History andPhilosophy of Logic, 20:1–31, 1999.

BIBLIOGRAPHY

85[32] Erik Sandewall. Features and Fluents: The Representation of Knowledge
about Dynamical Systems, volume 1. Oxford University Press, 1994.
[33] Murray Shanahan. An abductive event calculus planner. Journal of Logic
Programming, 44(1-3):207–240, 2000.
[34] Murray Shanahan and Mark Witkowski. High-level robot control throughlogic. Lecture Notes in Computer Science, 1986, 2001.
[35] Tran Cao Son, Chitta Baral, and Sheila McIlraith. Extending answer
set planning with sequence, conditional, loop, non-deterministic choice,and procedure constructs. In Proceedings of the AAAI Spring Symposium
on Answer Set Programming: Towards Efficient and Scalable Knowledge
Representation and Reasoning, pages 202–209, Stanford, ca, USA, March
26-28 2001.
[36] Michael Thielscher. FLUX webpage. http://www.fluxagent.org/. Visited December 2006.
[37] Michael Thielscher. FLUX: A logic programming method for reasoning
agents. Theory and Practice of Logic Programming, 5(4–5):533–565, 2005.
[38] John Thornton, Matthew Beaumont, Abdul Sattar, and Michael J. Maher. A local search approach to modelling and solving interval algebra
problems. Journal of Logic and Computation, 14(1):93–112, 2004.
[39] Wikipedia. Presburger arithmetic — wikipedia, the free encyclopedia,
2007. Visited January 2007.

86

BIBLIOGRAPHY

Avdelning, Institution
Division, Department

Datum
Date

AIICS,
Dept. of Computer and Information Science581 83 Linköping
SpråkRapporttyp
Report categoryISBN

Language Svenska/Swedish× Licentiatavhandling

ISRN

× Engelska/English

 Examensarbete
 C-uppsats
 D-uppsats Övrig rapport

2007-09-28

978–91–85895–93–9
LiU-Tek-Lic–2007:38
Serietitel och serienummer ISSN
Title of series, numbering
0280–7971


URL för elektronisk version

http://www.martinmagnusson.com/
publications/magnusson-2007-lic.pdf

Linköping Studies in Science and Technology
Thesis No. 1329

Titel
Title

Deductive Planning and Composite Actions in Temporal Action LogicFörfattare
AuthorMartin Magnusson
Sammanfattning
Abstract

Temporal Action Logic is a well established logical formalism for reasoning about action and change that has long been used as a formal specification language. Its first-order characterization and explicit time representation
makes it a suitable target for automated theorem proving and the applicationof temporal constraint solvers. We introduce a translation from a subset ofTemporal Action Logic to constraint logic programs that takes advantage ofthese characteristics to make the logic applicable, not just as a formal specification language, but in solving practical reasoning problems. Extensions
are introduced that enable the generation of action sequences, thus paving
the road for interesting applications in deductive planning. The use of qualitative temporal constraints makes it possible to follow a least commitment
strategy and construct partially ordered plans. Furthermore, the logical language and logic program translation is extended with the notion of composite
actions that can be used to formulate and execute scripted plans with conditional actions, non-deterministic choices, and loops. The resulting planner andreasoner is integrated with a graphical user interface in our autonomous helicopter research system and applied to logistics problems. Solution plans aresynthesized together with monitoring constraints that trigger the generationof recovery actions in cases of execution failures.

Nyckelord
Keywords

Temporal Action Logic, deductive planning, composite actions, interval
algebra, constraint logic programming, execution monitoring