O. Kahramanoğulları (Germany)
Planning, Concurrency, Proof theory
We present a purely logical framework to planning where we bring the sequential and parallel composition in the plans to the same level, as in process algebras. The prob lem of expressing causality, which is very challenging for common logics and traditional deductive systems, is solved by resorting to a recently developed extension of multi plicative exponential linear logic with a self-dual, non commutative operator. We present an encoding of the con junctive planning problems in this logic, and provide a con structive soundness and completeness result. We argue that this work is the first, but crucial, step of a uniform deduc tive formalism that connects planning and concurrency in side a common language, and allows to transfer methods from concurrency to planning.
Important Links:
Go Back
