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.

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

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

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

Fig. 10

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 G₁ to goals to achieve them later. Each label in Δ_O is incorporated to the G₁’s forbidden list, because those assumptions are not allowed to be used to achieve that goal. The d-⊗₁ rule uses D₁ to achieve a and adds D₂ to Δ_O. The d-⊗₂ rule uses D₂ 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

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.