## Abstract

In this paper, we propose an exponential multiplicative fragment of linear logic to encode and solve planning problems efficiently in STRIPS domain, that we call the Linear Planning Logic (LPL). Linear logic is a resource aware logic treating resources as single use assumptions, therefore enabling encoding and reasoning of domains with dynamic state. One of the most important examples of dynamic state domains is robotic task planning, since informational or physical states of a robot include non-monotonic characteristics. Our novel theorem prover is using the backchaining method which is suitable for logic languages like Lolli and Prolog. Additionally, we extend LPL to be able to encode non-atomic conclusions in program formulae. Following the introduction of the language, our theorem prover and its implementation, we present associated algorithmic properties through small but informative examples. Subsequently, we also present a navigation domain using the hexapod robot RHex to show LPL’s operation on a real robotic planning problem. Finally, we provide comparisons of LPL with two existing linear logic theorem provers, llprover and linTAP. We show that LPL outperforms these theorem provers for planning domains.

This is a preview of subscription content, log in to check access.

## References

- 1.
Arslan, O., Saranli, U.: Reactive planning and control of planar spring-mass running on rough terrain. IEEE Trans. Robot.

**28**(3), 567–579 (2012) - 2.
Belta, C., Bicchi, A., Egerstedt, M., Frazzoli, E., Klavins, E., Pappas, G.: Symbolic planning and control of robot motion - grand challenges of robotics. IEEE Robot. Autom. Mag.

**14**(1), 61–70 (2007) - 3.
Bimbó, K.: The decidability of the intensional fragment of classical linear logic. Theor. Comput. Sci.

**597**, 1–17 (2015) - 4.
Blum, A.L., Furst, M.L.: Fast planning through planning graph analysis. Artif. Intell.

**90**(1), 1636–1642 (1995) - 5.
Brachman, R., Levesque, H.: Knowledge Representation and Reasoning. Morgan Kaufmann Publishers Inc., San Francisco (2004)

- 6.
Cervesato, I., Hodas, J.S., Pfenning, F.: Efficient resource management for linear logic proof search. Theor. Comput. Sci.

**232**(1-2), 133–163 (2000) - 7.
Chrpa, L.: Linear logic in planning. In: Proceedings of the International Conference on Automated Planning and Scheduling, pp. 26–29 (2006)

- 8.
Conner, D., Choset, H., Rizzi, A.: Flow-through policies for hybrid controller synthesis applied to fully actuated systems. IEEE Trans. Robot.

**25**(1), 136–146 (2009) - 9.
Dimopoulos, Y., Nebel, B., Koehler, J.: Encoding planning problems in nonmonotonic logic programs. In: Steel, S., Alami, R. (eds.) Recent Advances in AI Planning, Lecture Notes in Computer Science, pp. 169–181. Springer (1348)

- 10.
Dixon, L., Bundy, A., Smaill, A.: Verified planning by deductive synthesis in intuitionistic linear logic. In: Proceedings of the Workshop on Verification and Validation of Planning and Scheduling Systems, p. 10 (2009)

- 11.
Dixon, L., Smaill, A., Tsang, T.: Plans, actions and dialogue using linear logic. J. Log. Lang. Inf.

**18**, 251–289 (2009) - 12.
Do, M.B., Kambhampati, S.: Planning as constraint satisfaction: Solving the planning graph by compiling it into CSP. Artif. Intell.

**132**(2), 151–182 (2001) - 13.
Eiter, T., Faber, W., Leone, N., Pfeifer, G., Polleres, A.: Answer set planning under action costs. J. Artif. Intell. Res.

**19**, 25–71 (2003) - 14.
Girard, J.Y.: Linear logic. Theor. Comput. Sci.

**50**(1), 1–102 (1987) - 15.
Gupta, N., Nau, D.S.: On the complexity of blocks-world planning. Artif. Intell.

**56**(2-3), 223–254 (1992) - 16.
Hodas, J.S., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Inf. Comput.

**110**(2), 327–365 (1994) - 17.
Jacopin, E.: Classical AI planning as theorem proving: the case of a fragment of linear logic. In: AAAI Fall Symposium on Automated Deduction in Nonstandard Logics, Palo Alto, CA (1993)

- 18.
Kahramanogullari, O.: Towards planning as concurrency. In: Artificial Intelligence and Applications, pp. 387–393 (2005)

- 19.
Kahramanoğulları, O.: On linear logic planning and concurrency. In: Language and Automata Theory and Applications, pp. 250–262. Springer (2008)

- 20.
Kanovich, M., Vauzeilles, J.: The classical AI planning problems in the mirror of horn linear logic: semantics, expressibility, complexity. Math. Struct. Comput. Sci.

**11**(6), 689–716 (2001) - 21.
Kanovich, M.I., Vauzeilles, J.: Linear logic as a tool for planning under temporal uncertainty. Theor. Comput. Sci.

**412**(20), 2072–2092 (2011) - 22.
Kortik, S., Saranli, U.: Linear planning logic: an efficient language and theorem prover for robotic task planning. In: Proceedings of the IEEE International Conference on Robotics and Automation, pp. 3764–3770 (2014)

- 23.
Kungas, P.: Linear Logic Programming for AI Planning. M.Sc., Institute of Cybernetic at Tallinn Technical University (2002)

- 24.
LaValle, S.M.: Planning Algorithms. Cambridge University Press, Cambridge (2006)

- 25.
Lee, J., Palla, R.: Reformulating the situation calculus and the event calculus in the general theory of stable models and in answer set programming. J. Artif. Intell. Res.

**43**, 571–620 (2012) - 26.
Lifschitz, V.: Answer set planning. In: Gelfond, M., Leone, N., Pfeifer, G. (eds.) Logic Programming and Nonmonotonic Reasoning, Lecture Notes in Computer Science, vol. 1730, pp. 373–374. Springer (1999)

- 27.
Lopez, A., Bacchus, F.: Generalizing GraphPlan by formulating planning as a CSP. In: Proceedings of the International Joint Confernece on Artificial Intelligence, pp. 954–960. Morgan Kaufmann Publishers Inc., San Francisco (2003)

- 28.
Lozano-Perez, T.: Task planning. In: Robot Motion Planning and Control, pp. 473–498. MIT Press, Cambridge (1982)

- 29.
Mantel, H., Otten, J.: lintap: a tableau prover for linear logic. In: Automated Reasoning with Analytic Tableaux and Related Methods, pp. 661–661 (1999)

- 30.
Martínez, D, Alenyáá, G., Torras, C.: Planning robot manipulation to clean planar surfaces. Eng. Appl. Artif. Intell.

**39**, 23–32 (2015) - 31.
Masseron, M., Tollu, C., Vauzeilles, J.: Generating plans in linear logic I. Actions as proofs. Theor. Comput. Sci.

**113**(2), 349–370 (1993) - 32.
McAllester, D., Rosenblitt, D.: Systematic nonlinear planning. In: Proceedings of the National Conference of the American Association for Artificial Intelligence (AAAI-91), pp. 634–639 (1991)

- 33.
McCarthy, J.: Situations, Actions, and Causal Laws. Tech. Rep AD0785031. Stanford University, Department of Computer Science (1963)

- 34.
Nau, D.S.: Current trends in automated planning. AI Mag.

**28**(4), 43 (2007) - 35.
Penberthy, J.S., Weld, D.S.: UCPOP: a sound, complete, partial order planner for ADL. In: Proceedings of the International Conference on Knowledge Representation and Reasoning, pp. 103–114 (1992)

- 36.
Pfenning, F.: Lecture Notes on Automated Theorem Proving. Technical report, Carnegie Mellon University (1999)

- 37.
Pfenning, F.: Lecture Notes on Linear Logic. Technical report, Carnegie Mellon University (2002)

- 38.
Reiter, R.: The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression. Artif. Intell. Math. Theory Comput.

**27**, 359–380 (1991) - 39.
Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach, 2nd edn. Prentice Hall, Englewood Cliffs (2003)

- 40.
Saranli, U., Buehler, M., Koditschek, D.E.: RHex: a simple and highly mobile robot. Int. J. Robot. Res.

**20**(7), 616–631 (2001) - 41.
Tamura, N.: User’s Guide of a Linear Logic Theorem Prover (Llprover). Tech. Rep., Department of Computer and Systems Engineering Faculty of Engineering. Kobe University, Japan (1998)

- 42.
Thompson, S.: Type Theory and Functional Programming. Addison-Wesley, Reading (1991)

- 43.
Vaquero, T.S., Silva, J.R., Beck, J.C.: Post-design analysis for building and refining AI planning systems. Eng. Appl. Artif. Intell.

**26**(8), 1967–1979 (2013)

## Acknowledgments

This work was supported by Tubitak project 114E277.

## Author information

### Affiliations

### Corresponding author

## Additional information

### Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

## Appendices

### Appendix A: Reduction (Right) Rules for the BL Proof Theory

Right rules for both simultaneous conjunction, linear implication and existential quantification are eagerly applied first, until the sequent’s conclusion is atomic. Associated rules are given in Fig. 8.

The ⊗ *R* rule relies on the I/O model to efficiently decompose available resources into left and right subgoals. In the right rule for linear implication, **bl-**\({\multimap }\), we try to achieve the subgoal *G* by using the assumption *D*. We should note that assumptions in Δ_{O} can not depend on the introduced assumption *D*. We need such a restriction, because the output context Δ_{O} is not a subset of Δ_{I} anymore.

In the **bl-**∃ rule, a term *t* is provided and then substituted for the variable *x*.

Figure 9 shows the reduction rule for classical implication. Occurrences of the \(D {\supset } G\) formula as a goal allow adding the resource *D* to the set of unrestricted resources G. Same as the **bl-**\({\multimap }\) rule, assumptions in Δ_{O} can not depend on *D*.

### Appendix B: Resolution Rules for the BL Proof Theory

In Fig. 10, we give both linear and unrestricted resolution rules for the BL language. Both rules have the important side condition that focusing on any of the forbidden resources is not allowed with *u*∉*F*. The input context of the first subgoal is the union of the input context Δ_{I} of the conclusion sequent, and the output context Δ_{O,0} from the residuation judgement.

Apart from these side conditions, the AddLb() function makes sure that, if the label of a resource in the final output context Δ_{O,n} is in the forbidden list *F*, then the dependence list of this resource is increased with *L* (dependence list) of *D* (focused resource). We formally define the AddLb() as

### Appendix C: Residuation Rules for the BL Proof Theory

Finally, Fig. 11 shows all the residuation rules in the BL proof system for LPL. The **bl-atm** rule succeeds if the atomic resource \(a^{\prime }\) can be unified with the atomic goal (*a*). The **d-**\({\multimap }\) rule attempts to achieve the atomic goal *a* with *D*, and then incorporates the goal *G*_{1} to goals to achieve them later. Each label in Δ_{O} is incorporated to the *G*_{1}’s forbidden list, because those assumptions are not allowed to be used to achieve that goal. The **d-**⊗_{1} rule uses *D*_{1} to achieve *a* and adds *D*_{2} to Δ_{O}. The **d-**⊗_{2} rule uses *D*_{2} to achieve the atomic *a*, and adds the other resource to Δ_{O}. The **d-**∀ rule achieves *a* by substituting all variables *x* with the term *t* in *D*. This term is expected to be globally chosen later through unification.

An important property of this newly defined residuation judgment for LPL is that the property \({\Delta }_{O} \subseteq {\Delta }_{I}\) is not necessarily satisfied, which deviated substantially from the backchaining proof theory provided for LHHF in [16]. In our case, Δ_{O} might have sub-formulas of certain resources in Δ_{I}, which is the conclusion of enabling simultaneous conjunction on left side of a formula. This observation is important in proving the soundness and completeness of the BL proof theory.

## Rights and permissions

## About this article

### Cite this article

Kortik, S., Saranli, U. Robotic Task Planning Using a Backchaining Theorem Prover for Multiplicative Exponential First-Order Linear Logic.
*J Intell Robot Syst* **96, **179–191 (2019). https://doi.org/10.1007/s10846-018-0971-9

Received:

Accepted:

Published:

Issue Date:

### Keywords

- Robotic task planning
- Linear logic
- Automated theorem proving
- Visual navigation
- Backchaining
- RHex hexapod