Linearity and plan generation (Q1108814)

The paper deals with the intuitive linearity concept and its weak points. This concept is commonly used at plan generation using theorem proving in which deduction of a goal statement is proved from the initial situation and rules describing the actions. A typical property of such a concept of linearity is that any literal in a proof is presented only once. Proofs linear in this sense, however, are changing to non-linear ones if the corresponding formulas has been transformed into normal form what is a condition for plan generation by existing theorem provers. The author is trying to suggest such linearity concepts which would overcome troubles connected with the transformation of general formulas into normal forms. As the first step towards an extended linearity concept the so called U-linearity is defined, which allows a multiple occuring of literals and multiple using the rules. To enable multiple connections (according to the connection method used) the concept of C- linearity is introduced, which by some new ``connector literals'' overcomes some of U-linearity limitations. The C-linearity concept is strong enough to generate some types of plans, but to be more applicable, it is required that the state of the world is ``complete with respect to facts and rules'', what is leading to involved new notions of fr- completeness and of numerical stability. This limitation of the world means a reduction of rules to Horn clauses. The last generalization of the linearity concept is called an A-linearity and requires to introduce a further type, so called ``absorbent'' literals. All these generalizations of the linearity concept are illustrated by suitable examples. Finally, a comparison is made to stress the strong points of the author's approach with some classical methods of plan generation such as of Green and STRIPS.