No label defined (Q3976054)

[For the entire collection see Zbl 0731.00025.] The paper contains an application of linear logic [\textit{J.-Y. Girard}, Theor. Comput Sci. 50, 1-102 (1987; Zbl 0625.03037)] to planification problems. Main result of the paper is: ``Every concrete action can be represented by a formal action and, vice versa, every formal action can be interpreted as a concrete action''. A ``concrete action'' is a sequence of elementary actions, whereas a formal action is a proof of a sequent \(A_ 1,\dots,A_ m\lvdash B\) in a linear theory based on the fragment of intuitionistic linear logic with the connectives \(\otimes\) (multiplicative conjunction) and \(\oplus\) (additive disjunction) only \((A_ 1,\dots,A_ m\) are atomic formulas and the proof contains logical axioms and rules, and transition axioms, i.e. closed sequents of the form \(C_ 1,\dots,C_ n\lvdash D\) with \(C_ 1,\dots,C_ n\) atomic formulas); the intuitive meaning of \(A_ 1,\dots,A_ m\lvdash B\) is to consume \(A_ 1,\dots,A_ m\) and produce \(B\). The paper considers the concept of ``pseudo-plan'', and shows how we may associate a pseudo-plan to every formal action; another important result of the paper is that a pseudo-plan is constructed from a formal action iff its orientation is a partial ordering. The authors show very well the potential power of linear logic in the study of planification problems: further developments in this direction are possible and welcome.