J-T RE: An Integrated Reasoning Environment and its Application to Timeline-based Planning Riccardo De Benedictis CNR - National Research Council of Italy, ISTC, Rome, Italy riccardo.debenedictis@istc.cnr.it Abstract. The application of classical artificial intelligence techniques to real- istic dynamic scenarios arises interesting challenges which require, often, the tailoring of state-of-the-art solvers to the specific domains. The introduction of a “light” and highly customizable framework allows to facilitate the way a high number of possible problems are addressed. This paper introduces the ongoing work for a novel domain-independent reasoning environment called J-T RE that takes its inspiration from Constraint Logic Programming flavoring it with Object Oriented features. The paper also addresses the customization of such an envi- ronment to a particular kind of automated planning, referred to as timeline-based, particularly suitable for complex domains. As a result, an alternative formaliza- tion of the timeline-based planning problem is proposed that allows for an in- teresting ability to solve both planning and scheduling problems in a uniform schema. 1 Introduction Planning is the abstract and explicit deliberation process that chooses and organizes actions by anticipating their expected outcomes [24]. The area of Artificial Intelligence (AI) that studies this deliberation process computationally is called automated planning. Among the different qualities a cognitive architecture should have, automated planning constitutes a mandatory one. This paper fits inside this context by introducing the ongoing work for a novel domain-independent reasoning environment, endowed with a special emphasis on au- tomated planning, called Timeline Reasoning Environment for Java (J-T RE1 ). Specifi- cally, J-T RE represents a general architecture for logic and constraint-based reasoning that brings together some key aspects of intelligent reasoning leaving freedom to spe- cific implementations on both constraint reasoning engines and resolution heuristics. The proposed architecture is characterized by a basic core that allows the definition of classic AI problems providing the possibility for defining particular “components” de- voted to the resolution of specific AI problems (in our case, timeline-based planning problems). The paper is structured as follow. Section 2 describes the J-T RE reasoning envi- ronment with a special attention to its basic core. Section 3 describes how the basic 1 The J-T RE environment is the tool that has been developed on purpose for performing re- search along my PhD route. core and the general solving procedure have been extended to provide timeline-based planning capabilities. Section 4 contains a generic discussion about some related ap- proaches while section 5 contains conclusions and a description of the current state of the environment. 2 The J-T RE Reasoning Environment J-T RE is the result of last years studies on timeline-based planning [14, 15] and its ap- plication on field [4]. The reason for introducing a new architecture is to obtain a “light” and general framework for the resolution of classic AI problems, which might provide a common glue for the definition of different problems, coming from different AI fields, yet sharing constraints among them. A complex cognitive architecture, for example, might handle both temporal and spatial problems. Although there exist efficient tempo- ral reasoners and spatial reasoners, the definition of constraints among these problems might be cumbersome and highly inefficient to be managed. The basic core of the J-T RE environment provides an object oriented virtual envi- ronment for the definition of objects and constraints among them. The aim here is to provide to the user a minimalistic core that should be both sufficiently expressive as well as easily extensible so as to adapt as much as possible to the most variety of user requirements. Similar to most object oriented environments, every object in the J-T RE environ- ment is an instance of a specific type. J-T RE distinguishes among primitive types (e.g., bools, numbers, enums, strings, etc.) and user defined complex types (e.g., robots, trucks, locations, etc.) endowed with their member variables (variables associated to a specific object of either primitive or complex type), constructors (a special type of subroutine called to create an instance of the complex type) and methods (subroutines associated with an object of a complex type). Defining a navigation problem, for example, might require the definition of a Location complex type having two numeric member variables x and y representing the coordinates of each Location instance. In the following, we will address objects and their member variables using a Java style dot notation (i.e., given a Location instance l, its x-coordinate will be expressed as l.x). Once objects are defined, J-T RE allows the definition of constraints among them. For example, in case the x-coordinate of a location l is partially known, the J-T RE user could assert a constraint such l.x ≤ 10. J-T RE considers constraints as logic propo- sitions and, as such, it allows the possibility for negating them (e.g., ¬l.x ≤ 5), for expressing conjunctions (e.g., l.x ≤ 10 ∧ l.x ≥ 5), disjunctions (e.g., l.x ≤ 5 ∨ l.x ≥ 10) and logic implications (e.g., l.x ≥ 10 → l.y ≥ 10). Furthermore, it is possible to impose constraints on instance existential (e.g., ∃l ∈ Locations : l.x ≥ 10) and universal (e.g., ∀l ∈ Locations : l.x ≤ 100) quantifiers. It is worth noting that, in case the defined con- straints are inconsistent among themselves (e.g., l.x ≤ 10 ∧ l.x ≥ 15) the system will return a failure. A rather straightforward method for managing this kind of problems is to translate them into a Satisfiability Modulo Theories (SMT) problem (see, for example, [29]). There are several available SMT solvers having different performances, capabilities as well as licenses. Since J-T RE has been written in Java the only available choices are, to the best of our knowledge, the SMTInterpol [9], the MathSAT 5 [11] and the Z3 [16] solvers2 . Although this basic core allows the definition of quite complex problems (with- out providing any demonstration, we can state that all NP-Complete [22] problems are covered), some of the planning problems we are interested in are excluded from the possibility of being modelled with this formalism ([13], for example, traces a thresh- old on planning problems that can be modelled with what we have shown till now). In order to overcome these limitations, we need something more powerful. Something that, roughly speaking, is able to “decide” the number of involved variables, together with their value. For this purpose, we have chosen to endow complex types the possi- bility to define predicate schemas over them (and, consequently, predicate instances on type instances). Intuitively, these predicate schemas are intended to define in which case their instances are logically true. An example of predicate schema that might be used for describing locations in the first quadrant of a Cartesian coordinate sys- tem is FirstQuadrant (Location l) ⇒ {l.x ≥ 0 ∧ l.y ≥ 0}. By creating a FirstQuadrant “query”, J-T RE will create a new FirstQuadrant predicate instance and will assign a location to its l variable such that its coordinates belong to the first quadrant of the Cartesian coordinate system. If such location does not exists, the system will return a failure. Similarly to standard objects, J-T RE allows the possibility to impose constraints on predicate instances as well. Moreover, it is worth to note that predicate schemas might include other predicate “queries” with a different predicate schema, possibly defined on other complex types, or even the same predicate schema (in the latter case we talk of a recursive definition of the predicate schema)3 . In both cases the system will require some form of subgoaling during the reasoning process. Finally, when possible, two predicate instances might be “unified” by the reasoner meaning that, from now on, the two predicates will be considered as a unique object (i.e., the reasoner puts bindings among their variables). In the following we provide some formal definition of the concept informally intro- duced till now. Definition 1. Given n complex types T = {T0 , . . . , Tn }, a domain theory D = {c0 , . . . , cm } is the collection of the predicate schemas defined over T . A predicate schema is a tuple c = (name (c) , R (c)), where: – name (c) is the master (or reference) predicate and is an expression of the form n (x0 . . . xk ), where n is a unique predicate symbol with respect to a complex type (i.e., no two predicate schemas in a given complex type can have the same predicate symbol), and x0 . . . xk are its associated variable symbols having either primitive types or complex types (in the latter case the variable will be considered as an existential quantifier). 2 While SMTInterpol provides a pure Java implementation, MathSAT and Z3 provide Java wrappers to their native API. We have not found other SMT solvers that provide, directly or indirectly, a Java API. 3 Recursive definitions produce a remarkably increase in expressiveness with the predictable side effect of a decrease in performances. – R (c) is a requirement, i.e. either a slave (or target) predicate, a constraint, a con- junction of requirements, a disjunction of requirements or a preferred requirement. In this regard, it is worth to recall that constraints can be combined in any logical combination (i.e., negations, disjunctions, etc.). Definition 2. A predicate instance is an expression of the form: n (x0 , . . . , xk ) where n is a predicate name and x0 , . . . , xk are constants, numeric variables or object variables. The set of objects, predicate instances and constraints among objects and/or predi- cate instances is called a partial solution and, as we shall soon, will be used to represent nodes of the J-T RE search space. More formally we have that: Definition 3. A partial solution is a tuple π = (O, T,C), where: – O={ {o0 , . . . , o} i } is a set of objects. – T = t0 , . . . ,t j is a set of predicate instances. – C is a set of constraints on objects and/or on variables of predicate instances in T . C is required to be consistent, i.e., there exist values for all the variables that meet all the constraints. Moreover, since the real world has high degrees of uncertainty, we might be interested in maintaining different possible solutions in a single partial solution. Finally, given a domain theory D, a set of objects O, we can reuse the concept of requirement for defining a J-T RE problem, i.e. either a slave (or, in the case of a problem, a goal) predicate, a constraint, a conjunction of requirements, a disjunction of requirements or a preferred requirement. Definition 4. A problem is a tuple P = (D, O, R), where: – D is a domain theory. – O = {o0 , . . . , ok } is a set of objects. – R is a requirement. From an operational point of view, J-T RE uses an adaptation of the resolution prin- ciple [28] extended for managing constraints in a more general scheme usually known as constraint logic programming (CLP) [1]. More in general, we give the name flaw to anything that keeps the current partial solution from being a solution. While flaws can be of different types and can arise for different reasons, what they all have in common is that a search choice is necessary to solve each of them, thus the basic operations for refining a partial solution π toward a solution are the following: 1. find the flaws of π , i.e., its subgoals. 2. select one such flaw. 3. find ways to resolve it. 4. choose a resolver for the flaw. 5. refine π according to that resolver. Starting from an initial node corresponding to an empty solution, the search aims at a final node containing a solution that correctly achieves the required goals, i.e, when there is no flaw in π and all of its constraints are consistent then π is a solution. When possible, resolution will try to unify goals with existing predicate instances, creating a branch for all possible unifications. In case unification is not possible, resolution will create a new branch of the search space, will create a new predicate instance, will find a predicate schema suitable for the instance and will apply it. How can such a generic framework be related with automated planning? Is it pos- sible to extend the framework to manage other forms of reasoning? In the following, after some basic introductory information on classical and timeline-based planning, we will try to convince the reader that it is possible to give an affirmative answer to these questions. 3 Timeline-based Planning and J-T RE Classical planning4 approaches the planning problem as the search for a path in the graph of a state-transition system [17], thus, the search space is given directly by the state-transition system: nodes are states of the domain; arcs are state transitions or ac- tions; a plan is a sequence of actions corresponding to a path from the initial state to a goal state. The timeline-based approach to planning represents an effective alternative to clas- sical planning for complex domains requiring the use of both temporal reasoning and scheduling features. The timeline-based approach models the planning and scheduling problem by identifying a set of relevant features of the planning domain which need to be controlled to obtain a desired temporal behaviour. Timelines model entities whose properties may vary in time and which represent one or more physical (or logical) sub- systems which are relevant to a given planning context. The planner/scheduler plays the role of the controller for these entities, and reasons in terms of constraints that bound their internal evolutions and the desired properties of the generated behaviours. Most of the timeline-based planners use a more elaborate search space that is not the state-transition system anymore. Their search space has partially specified plans as nodes and plan refinement operations as arcs. Plan refinement operations are intended to further complete a partial solution, i.e., to achieve an open goal or to remove some possible inconsistency. Intuitively, these refinement operations avoid adding to the par- tial plan any constraint that is not strictly needed for addressing the refinement purpose (this is called the least commitment principle). The solving procedure starts from an ini- tial node corresponding to an empty solution. The search aims at a final node containing a solution that correctly achieves the required goals. Given these premises, a possible approach to the resolution of timeline-based plan- ning problems is to provide the predicate instances introduced in the previous section with numerical variables in order to represent their starting times, their ending times 4 Classical planning is also referred to in the literature as STRIPS planning, in reference to STRIPS, an early planner for restricted state-transition systems [18]. and their durations. Also, it will be required to define some specific complex types, whose instances will be called timelines, in order to add further “implicit” constraints on the predicate instances defined over their instances. Finally, we need to enhance the resolution procedure in order to check the consistency for every object in the current partial solution so as to make explicit the just mentioned implicit constraints. (a) State variable (b) Reusable resource (c) Consumable resource Fig. 1. Different kinds of timelines with predicate instances and resource profiles. The minimal set of the complex types, commonly used in timeline-based planning, is the following: – State variables are used to describe the “state” of a dynamical system as, for ex- ample, the position of a specific object at a given time or a simple manufacturing tool that might be operating or not. The semantics of a state variable (and thus the implicit constraints on predicate instances associated to it) is simply that, for each time instant t ∈ T, the timeline can assume only one value. State variable predicate schemas are defined by the user during domain definition (temporal parameters are implicitly defined). Figure 1(a) represents an example of state variable with three predicate instances. – Resources are characterized by a resource level L : T → R, representing the amount of available resource at any given time, and by a resource capacity C ∈ R, repre- senting the physical limit of the available resource. We can identify several types of resources depending on how the resource level can be increased or decreased in time. A consumable resource is a resource whose level is increased or decreased by some activities in the system. An example of consumable resource is a reservoir which is produced when a plan activity “fills” it (i.e., a tank refueling task) as well as consumed if a plan activity “empties” it (i.e., driving a car uses gas). Consumable resources have two empty predicate schemas having a predicate Produce (a, s, e, d) to represent a resource production of amount a from time s to time e with duration d, and a predicate Consume (a, s, e, d) to represent a resource consumption of amount a from time s to time e with duration d. In addition, consumable resources have four member variables representing the initial and the final amount of the resource, the min and the max value for the profile. Reusable resources have one empty predicate schema having a predicate Use (a, s, e, d) that represent an instantaneous production of resource of amount a at time s and an instantaneous consumption of resource of the same amount a at time e (e.g., a given number of programmers employed on a given project for a given time interval). Reusable resources have a single member variable representing the capacity of the resource. Figures 1(c) and 1(b) represent, respectively, an example of consumable resource and an example of reusable resource with some associated predicate instances. By introducing these complex types, we require the reasoner to identify an ordering of the involved predicate instances in order to avoid object inconsistencies (e.g., dif- ferent states overlapping on some state variable; resource levels L exceeding resource capacity C or going lower than zero, etc.). The aim of the reasoner becomes now to find a legal state of the predicate instances that brings the objects into a final configuration that verifies domain theory, goals and implicit constraints. Nodes of the search space are still partially specified solutions while arcs are problem refinement operations intended to further complete a partial solution, i.e., to achieve an open goal (by applying the “consequences” of the goal as defined in the associated predicate schema), to remove a possible object inconsistency (e.g., by adding some further constraint), to chose a disjunct among a disjunction or to chose whether to satisfy a preference or not. We just need to redefine the concept of flaw so as to include the just introduced object inconsistencies. Definition 5. A flaw in a partial solution π = (O, T,C) is either: (i) an open goal, (ii) an object inconsistency, (iii) a disjunction or (iv) a preference. As expected, the refinement operations avoid adding to the partial solutions con- straints that are not strictly needed following preserving the least commitment princi- ple. Starting from an initial node corresponding to an empty solution, the search aims at a final node containing a solution that correctly achieves the required goals. This algo- rithm (specified as a recursive non-deterministic schema in Figure 2) represents a slight adaptation of the classical Partial Order Planning algorithm (see, for example, [30]). procedure S OLVE(π ) f laws ← OpenGoals (π ) ∪ Inconsistencies (π ) ∪ Disjs (π ) ∪ Prefs (π ) if f laws = 0/ then return π select any flaw ϕ ∈ f laws resolvers ← Resolve (ϕ , π ) if resolvers = 0/ then return ⊥ non-deterministically choose a resolver ρ ∈ resolvers π ′ ← Refine (ρ , π ) return Solve (π ′ ) Fig. 2. The J-T RE solving procedure. 4 General Discussion There is plenty of related literature which achieve different results from those presented in this paper. The concept of predicate schema has its roots in the research on automatic theorem proving. Exception made for mathematical constraints, predicate schemas are very similar to standard Logic Programming (LP) clauses. Although standard Prolog implementations allow the imposition of mathematical constraints, imposing such con- straints in a general manner would possibly lead to run-time errors since arithmetic tests can be made only if the arguments are instantiated. Constraint Logic Program- ming overcomes this limitation by extending LP so as to allow linear constraints over real variables CLP(R) (with namesake implementation [25]) and among variables rang- ing over finite domains CLP(FD) (like ECLi PSe [1], SWI-Prolog [31] and many others). Many results have been achieved also with regard to the timeline-based planning. Similar to what has been described in this paper, [10] proposes a theoretical formal- ism (and the relative implementation) for the timeline-based planning problem. [12] exploits SMT technology to address a similar problem, also taking into account tempo- ral uncertainty. Some theoretical work on timeline-based planning like [20] was mostly dedicated to explain details of E UROPA [26], or to identify connections with classical planning a-la PDDL [19]. The work on A SPEN [8], IxTET [23] and T RF [21, 5] have tried to clarify some key underlying principles but mostly succeeded in underscoring the role of time and resource reasoning [7, 27]. The object oriented environment, provided by J-T RE, allows an easy customization for specific problems, such those required for timeline-based planning, yet maintaining a shared glue, made by a uniform resolution procedure and a unified constraint prop- agation infrastructure, among the different problems. This flexibility could be highly appreciated when using the tool in real contexts. The search control part has always remained significantly under explored. The cur- rent realm is that although these planners capture elements that are very relevant for applications, their theories are often quite challenging from a computational point of view and their performance are rather weak compared with those of state of the art classical planners. Indeed, timeline-based planners are mostly based on the notion of partial order planning [30] and have almost neglected advantages in classical planning triggered from the use of G RAPH P LAN and/or modern heuristic search [2, 3]. Further- more, these architectures rely on a clear distinction between temporal reasoning and other forms of constraint reasoning and there is no sign of attempts to change. Constraint disjunctions, provided by the underlying SMT solver, should be ex- ploited as much as possible. When available, for example, the J-T RE solver creates a disjunction of all possible unifications for a goal. Temporal mutual exclusion for state variable predicate instances, as well as overproductions and overconsumptions of re- sources, could be handled, without resorting to the concept of flaw, by imposing tem- poral disjunctions. The reason for preferring disjunctions to flaws is that SMT solvers have their own internal search space that is highly optimized thanks to state-of-the-art techniques such as backjumping and nogood learning. It is not yet clear if (and how) backjumping and nogood learning techniques could be applied to the J-T RE search procedure. 5 Conclusions and current status This paper presents the ongoing work on J-T RE, a novel domain-independent reasoning environment, and its particular customization to a timeline-based planning domain. We have proposed a constraint-logic based formalism for the J-T RE reasoner and we have seen that it can be easily extended to the timeline-based case. Despite the practical use of timeline-based planning is often more intuitive than classical planning, these kind of planners have to cope with performance issues due to the complexity that derives from their expressiveness. The use of Satisfiability Modulo Theories (SMT) for performing constraint propagation and for managing disjunctions has proved to be effective for solving these kinds of problems. We are currently work- ing on the development of benchmark problems for the proposed formalism as well as translators from other planning languages such as PDDL2.1 [19] and later versions. Despite the reasoner has not been extensively tested yet, [6] contains some promising initial results. Finally, unlike [12] we do not (yet) account uncertainty in our domains. Thanks to its domain causality and its constraint reasoning capabilities, J-T RE has been successfully used as the back-end reasoner for the PANDORA European project to create, reproduce and adapt a crisis scenario simulation suitable for the psychophysi- ological state of the involved users (see [4] for further details). Since the complexity of the possible interactions of an intelligent system with a real environment might be overly complex to be encoded in predicate schemas, inside the PANDORA project we have supported J-T RE with machine learning techniques so as to achieve an high level interpretation of psychophysiological features and user classification. A tighter integra- tion of these technologies might be further investigated in order to reach a more com- plex cognitive architecture that might be able to perform complex tasks in a dynamic environment. Acknowledgements I am thankful to the Planning and Scheduling Technology Laboratory (PST) and especially its coordinator Amedeo Cesta. My studies are partially supported by EU under the GiraffPlus Project (contract #288173. FP7 - ICT - Challenge 5) and by MIUR/CNR under Flagship Initiative FdF-SP1-T2.1 - GECKO Project. References 1. Apt, K.R., Wallace, M.G.: Constraint Logic Programming Using ECLi PSe . Cambridge Uni- versity Press, New York, NY, USA (2007) 2. Blum, A., Furst, M.L.: Fast Planning Through Planning Graph Analysis. In: IJCAI. pp. 1636– 1642. Morgan Kaufmann (1995) 3. Bonet, B., Geffner, H.: Planning as Heuristic Search. Artificial Intelligence 129(12), 5–33 (2001) 4. Cesta, A., Cortellessa, G., Benedictis, R.D.: Training for Crisis Decision Making - An Ap- proach Based on Plan Adaptation. Knowledge-Based Systems 58, 98–112 (2014) 5. Cesta, A., Cortellessa, G., Fratini, S., Oddi, A.: Developing an End-to-End Planning Ap- plication from a Timeline Representation Framework. In: IAAI-09. Proceedings of the 21st Innovative Applications of Artificial Intelligence Conference, Pasadena, CA, USA (2009) 6. Cesta, A., De Benedictis, R., Orlandini, A., Umbrico, A., Bernardi, G.: Integrating Planning and Scheduling Capabilities in a Space Robotics Domain. In: ASTRA 2013 - 12th Sympo- sium on Advanced Space Technologies in Robotics and Automation. vol. 12. ESA (2013) 7. Cesta, A., Oddi, A.: Gaining Efficiency and Flexibility in the Simple Temporal Problem. In: Chittaro, L., Goodwin, S., Hamilton, H., Montanari, A. (eds.) Proceedings of the Third Inter- national Workshop on Temporal Representation and Reasoning (TIME-96). IEEE Computer Society Press: Los Alamitos, CA (1996) 8. Chien, S., Tran, D., Rabideau, G., Schaffer, S., Mandl, D., Frye, S.: Timeline-Based Space Operations Scheduling with External Constraints. In: ICAPS-10. Proc. of the 20th Int. Conf. on Automated Planning and Scheduling (2010) 9. Christ, J., Hoenicke, J., Nutz, A.: Smtinterpol: An interpolating SMT solver. In: Model Checking Software - 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings. pp. 248–254 (2012) 10. Cialdea Mayer, M., Umbrico, A., Orlandini, A.: A Formal Account of Planning with Flexible Timelines. In: 21st International Symposium on Temporal Representation and Reasoning (TIME 2014) (2014) 11. Cimatti, A., Griggio, A., Schaafsma, B., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N., Smolka, S. (eds.) Proceedings of TACAS. LNCS, vol. 7795. Springer (2013) 12. Cimatti, A., Micheli, A., Roveri, M.: Timelines with Temporal Uncertainty. In: AAAI (2013) 13. Cushing, W., Kambhampati, S., Mausam, Weld, D.S.: When is temporal planning really temporal? In: Proceedings of the 20th International Joint Conference on Artifical Intelli- gence. pp. 1852–1859. IJCAI’07, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (2007) 14. De Benedictis, R., Cesta, A.: New Reasoning for Timeline based Planning - An Introduction to J-TRE and its Features. In: ICAART 2012 - 4th International Conference on Agents and Artificial Intelligence. pp. 144–153. SciTePress (2012) 15. De Benedictis, R., Cesta, A.: Timeline Planning in the J-TRE Environment. In: Felipe, J., Fred, A. (eds.) Agents and Artificial Intelligence. ICAART 2012 Revised Selected Papers, vol. 358, p. 218233. Springer Berlin Heidelberg (2013) 16. De Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Con- struction and Analysis of Systems. pp. 337–340. TACAS’08/ETAPS’08, Springer-Verlag, Berlin, Heidelberg (2008) 17. Dean, T.L., Wellman, M.P.: Planning and Control. Morgan Kaufmann Publishers Inc. (1991) 18. Fikes, R., Nilsson, N.J.: STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving. In: IJCAI. pp. 608–620 (1971) 19. Fox, M., Long, D.: PDDL2.1: An Extension to PDDL for Expressing Temporal Planning Domains. Journal of Artificial Intelligence Research 20, 61–124 (2003) 20. Frank, J., Jónsson, A.K.: Constraint-Based Attribute and Interval Planning. Constraints 8(4), 339–364 (2003) 21. Fratini, S., Pecora, F., Cesta, A.: Unifying Planning and Scheduling as Timelines in a Component-Based Perspective. Archives of Control Sciences 18(2), 231–271 (2008) 22. Garey, M.R., Johnson, D.S.: Computers and Intractability; A Guide to the Theory of NP- Completeness. W. H. Freeman & Co., New York, NY, USA (1990) 23. Ghallab, M., Laruelle, H.: Representation and Control in IxTeT, a Temporal Planner. In: AIPS-94. Proceedings of the 2nd Int. Conf. on AI Planning and Scheduling. pp. 61–67 (1994) 24. Ghallab, M., Nau, D., Traverso, P.: Automated Planning: Theory and Practice. Morgan Kauf- mann Publishers Inc. (2004) 25. Jaffar, J., Michaylov, S., Stuckey, P.J., Yap, R.H.C.: The CLP( R ) Language and System. ACM Transactions on Programming Languages and Systems 14(3), 339–395 (May 1992), http://doi.acm.org/10.1145/129393.129398 26. Jonsson, A., Morris, P., Muscettola, N., Rajan, K., Smith, B.: Planning in Interplanetary Space: Theory and Practice. In: AIPS-00. Proceedings of the Fifth Int. Conf. on AI Planning and Scheduling (2000) 27. Laborie, P.: Algorithms for propagating resource constraints in AI planning and scheduling: existing approaches and new results. Artificial Intelligence 143, 151–188 (February 2003) 28. Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle. Journal of the Association for Computing Machinery 12(1), 23–41 (1965) 29. Sebastiani, R.: Lazy Satisability Modulo Theories. JSAT 3, 141–224 (2007) 30. Weld, D.S.: An Introduction to Least Commitment Planning. AI Magazine 15(4), 27–61 (1994) 31. Wielemaker, J., Schrijvers, T., Triska, M., Lager, T.: SWI-Prolog. Theory and Practice of Logic Programming 12(1-2), 67–96 (2012)