# Robotic Task Planning Using a Backchaining Theorem Prover for Multiplicative Exponential First-Order Linear Logic

- 22 Downloads

## 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.

## Keywords

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

Unable to display preview. Download preview PDF.

## Notes

### Acknowledgments

This work was supported by Tubitak project 114E277.

## 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)CrossRefGoogle Scholar - 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)CrossRefGoogle Scholar - 3.Bimbó, K.: The decidability of the intensional fragment of classical linear logic. Theor. Comput. Sci.
**597**, 1–17 (2015)MathSciNetCrossRefGoogle Scholar - 4.Blum, A.L., Furst, M.L.: Fast planning through planning graph analysis. Artif. Intell.
**90**(1), 1636–1642 (1995)Google Scholar - 5.Brachman, R., Levesque, H.: Knowledge Representation and Reasoning. Morgan Kaufmann Publishers Inc., San Francisco (2004)zbMATHGoogle Scholar
- 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)MathSciNetCrossRefGoogle Scholar - 7.Chrpa, L.: Linear logic in planning. In: Proceedings of the International Conference on Automated Planning and Scheduling, pp. 26–29 (2006)Google Scholar
- 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)CrossRefGoogle Scholar - 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)Google Scholar
- 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)Google Scholar
- 11.Dixon, L., Smaill, A., Tsang, T.: Plans, actions and dialogue using linear logic. J. Log. Lang. Inf.
**18**, 251–289 (2009)MathSciNetCrossRefGoogle Scholar - 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)MathSciNetCrossRefGoogle Scholar - 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)MathSciNetCrossRefGoogle Scholar - 14.Girard, J.Y.: Linear logic. Theor. Comput. Sci.
**50**(1), 1–102 (1987)MathSciNetCrossRefGoogle Scholar - 15.Gupta, N., Nau, D.S.: On the complexity of blocks-world planning. Artif. Intell.
**56**(2-3), 223–254 (1992)MathSciNetCrossRefGoogle Scholar - 16.Hodas, J.S., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Inf. Comput.
**110**(2), 327–365 (1994)MathSciNetCrossRefGoogle Scholar - 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)Google Scholar
- 18.Kahramanogullari, O.: Towards planning as concurrency. In: Artificial Intelligence and Applications, pp. 387–393 (2005)Google Scholar
- 19.Kahramanoğulları, O.: On linear logic planning and concurrency. In: Language and Automata Theory and Applications, pp. 250–262. Springer (2008)Google Scholar
- 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)MathSciNetCrossRefGoogle Scholar - 21.Kanovich, M.I., Vauzeilles, J.: Linear logic as a tool for planning under temporal uncertainty. Theor. Comput. Sci.
**412**(20), 2072–2092 (2011)MathSciNetCrossRefGoogle Scholar - 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)Google Scholar
- 23.Kungas, P.: Linear Logic Programming for AI Planning. M.Sc., Institute of Cybernetic at Tallinn Technical University (2002)Google Scholar
- 24.LaValle, S.M.: Planning Algorithms. Cambridge University Press, Cambridge (2006)Google Scholar
- 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)MathSciNetCrossRefGoogle Scholar - 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)Google Scholar
- 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)Google Scholar
- 28.Lozano-Perez, T.: Task planning. In: Robot Motion Planning and Control, pp. 473–498. MIT Press, Cambridge (1982)Google Scholar
- 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)Google Scholar
- 30.Martínez, D, Alenyáá, G., Torras, C.: Planning robot manipulation to clean planar surfaces. Eng. Appl. Artif. Intell.
**39**, 23–32 (2015)CrossRefGoogle Scholar - 31.Masseron, M., Tollu, C., Vauzeilles, J.: Generating plans in linear logic I. Actions as proofs. Theor. Comput. Sci.
**113**(2), 349–370 (1993)MathSciNetCrossRefGoogle Scholar - 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)Google Scholar
- 33.McCarthy, J.: Situations, Actions, and Causal Laws. Tech. Rep AD0785031. Stanford University, Department of Computer Science (1963)Google Scholar
- 34.Nau, D.S.: Current trends in automated planning. AI Mag.
**28**(4), 43 (2007)Google Scholar - 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)Google Scholar
- 36.Pfenning, F.: Lecture Notes on Automated Theorem Proving. Technical report, Carnegie Mellon University (1999)Google Scholar
- 37.Pfenning, F.: Lecture Notes on Linear Logic. Technical report, Carnegie Mellon University (2002)Google Scholar
- 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)MathSciNetCrossRefGoogle Scholar - 39.Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach, 2nd edn. Prentice Hall, Englewood Cliffs (2003)Google Scholar
- 40.Saranli, U., Buehler, M., Koditschek, D.E.: RHex: a simple and highly mobile robot. Int. J. Robot. Res.
**20**(7), 616–631 (2001)CrossRefGoogle Scholar - 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)Google Scholar
- 42.Thompson, S.: Type Theory and Functional Programming. Addison-Wesley, Reading (1991)zbMATHGoogle Scholar
- 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)CrossRefGoogle Scholar