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

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

    Article  Google Scholar 

  2. 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)

    Article  Google Scholar 

  3. 3.

    Bimbó, K.: The decidability of the intensional fragment of classical linear logic. Theor. Comput. Sci. 597, 1–17 (2015)

    MathSciNet  Article  Google Scholar 

  4. 4.

    Blum, A.L., Furst, M.L.: Fast planning through planning graph analysis. Artif. Intell. 90(1), 1636–1642 (1995)

    Google Scholar 

  5. 5.

    Brachman, R., Levesque, H.: Knowledge Representation and Reasoning. Morgan Kaufmann Publishers Inc., San Francisco (2004)

    Google Scholar 

  6. 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)

    MathSciNet  Article  Google Scholar 

  7. 7.

    Chrpa, L.: Linear logic in planning. In: Proceedings of the International Conference on Automated Planning and Scheduling, pp. 26–29 (2006)

  8. 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)

    Article  Google Scholar 

  9. 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. 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. 11.

    Dixon, L., Smaill, A., Tsang, T.: Plans, actions and dialogue using linear logic. J. Log. Lang. Inf. 18, 251–289 (2009)

    MathSciNet  Article  Google Scholar 

  12. 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)

    MathSciNet  Article  Google Scholar 

  13. 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)

    MathSciNet  Article  Google Scholar 

  14. 14.

    Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50(1), 1–102 (1987)

    MathSciNet  Article  Google Scholar 

  15. 15.

    Gupta, N., Nau, D.S.: On the complexity of blocks-world planning. Artif. Intell. 56(2-3), 223–254 (1992)

    MathSciNet  Article  Google Scholar 

  16. 16.

    Hodas, J.S., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Inf. Comput. 110 (2), 327–365 (1994)

    MathSciNet  Article  Google Scholar 

  17. 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. 18.

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

  19. 19.

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

  20. 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)

    MathSciNet  Article  Google Scholar 

  21. 21.

    Kanovich, M.I., Vauzeilles, J.: Linear logic as a tool for planning under temporal uncertainty. Theor. Comput. Sci. 412(20), 2072–2092 (2011)

    MathSciNet  Article  Google Scholar 

  22. 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. 23.

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

  24. 24.

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

  25. 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)

    MathSciNet  Article  Google Scholar 

  26. 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. 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. 28.

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

  29. 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. 30.

    Martínez, D, Alenyáá, G., Torras, C.: Planning robot manipulation to clean planar surfaces. Eng. Appl. Artif. Intell. 39, 23–32 (2015)

    Article  Google Scholar 

  31. 31.

    Masseron, M., Tollu, C., Vauzeilles, J.: Generating plans in linear logic I. Actions as proofs. Theor. Comput. Sci. 113(2), 349–370 (1993)

    MathSciNet  Article  Google Scholar 

  32. 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. 33.

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

  34. 34.

    Nau, D.S.: Current trends in automated planning. AI Mag. 28(4), 43 (2007)

    Google Scholar 

  35. 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. 36.

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

  37. 37.

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

  38. 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)

    MathSciNet  Article  Google Scholar 

  39. 39.

    Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach, 2nd edn. Prentice Hall, Englewood Cliffs (2003)

  40. 40.

    Saranli, U., Buehler, M., Koditschek, D.E.: RHex: a simple and highly mobile robot. Int. J. Robot. Res. 20(7), 616–631 (2001)

    Article  Google Scholar 

  41. 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. 42.

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

    Google Scholar 

  43. 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)

    Article  Google Scholar 

Download references

Acknowledgments

This work was supported by Tubitak project 114E277.

Author information

Affiliations

Authors

Corresponding author

Correspondence to Sitar Kortik.

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.

Fig. 8
figure8

Right sequent rules for multiplicative connectives in the BL proof theory

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.

Fig. 9
figure9

Right sequent rules for classical implication in the BL proof theory

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

Fig. 10
figure10

Resolution rules for atomic goals for the BL proof system for LPL

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

$$\begin{array}{@{}rcl@{}} {{\text{AddLb}}}(L, \Delta, F) \!\!&:=&\!\! \left\{\vphantom{\left\{ \begin{array}{ll} L_{i} \cup L & \text{if}u_{i} \in F \\ L_{i} & \text{otherwise} \end{array} \right\}} ({u_{i}}:{}^{\bar{L_{i}}}{D_{i}})|({u_{i}}:{}^{L_{i}}{D_{i}}) \in \Delta,\text{and}\bar{L_{i}}\right.\\ &&{\kern-14.6pt}\left. = \left\{ \begin{array}{ll} L_{i} \cup L & \text{if}u_{i} \in F \\ L_{i} & \text{otherwise} \end{array} \right\}\!\right\}\!. \end{array} $$

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 G1 to goals to achieve them later. Each label in ΔO is incorporated to the G1’s forbidden list, because those assumptions are not allowed to be used to achieve that goal. The d-1 rule uses D1 to achieve a and adds D2 to ΔO. The d-2 rule uses D2 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.

Fig. 11
figure11

Residuation rules for atomic goals for the BL proof system for LPL

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

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

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

Download citation

Keywords

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