Generating plans in linear logic. I: Actions as proofs (Q1802077)

The paper is a revised and extended version of a previous one [the authors, Lect. Notes Comput. Sci. 472, 63-75 (1990; Zbl 0758.03017)]. It deals with an application of linear logic [\textit{J. Y. Girard}, Theor. Comput. Sci. 50, 1-102 (1987; Zbl 0625.03037)] to the planification problems. The main result 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 \vdash 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 \vdash D\) with \(C_ 1,\dots,C_ n\) atomic formulas); the intuitive meaning of \(A_ 1,\dots,A_ m \vdash B\) is to consume \(A_ 1,\dots, A_ m\) and produce \(B\). Two preliminary sections are devoted to the specification of the problems of planification and to the set-theoretic construction of concrete actions. The authors show very well the potential of linear logic in the study of planification problems: further developments in this direction are possible and welcome.