One of the main problems facing practical deployment of planners based on pure logical reasoning is the well-known frame problem. The origin of this problem can be traced back to the monotonicity of reasoning within classical logic, wherein knowledge never disappears and must be indexed by time to implement a representation of temporal progress. On the other hand, intuitionistic linear logic, due to its rejection of the structural rules of contraction and weakening, allows us to treat hypotheses as consumable resources and approximate temporal progress through a logical proof. Even though it has no inherent support for a metric treatment of temporal concepts, it still offers an elegant, but most importantly, tractable way of dealing with action planning problems within a logical formalism.

Many aspects of robotic planning problems require reasoning with continuous aspects of underlying systems. Especially for robots with significant dynamics, abstractions of primitive actions to be used by the planner must be sufficiently descriptive and accurate to ensure the physical relevance of returned action sequences. Even though various formalizations of intuitionistic linear logic can be expressive enough to capture such properties through axiomatizations of relevant continuous domains, such representations quickly lose their tractability and hence become unusable for practical systems.

Our approach is to extend linear logic with two new connectives that can be used to combine linear logical expressions with constraints drawn from a possibly continuous domain for which an efficient constraint solver is available. This is close in spirit to Constraint Logic Programming, which also interfaces proof theoretic reasoning with domain specific constraint solvers. In the presence of a well-defined semantic structure, this enables us to draw formal conclusions about the physical meaning of proofs interpreted as plans, resulting in a framework in which synthesized behaviors can have provable correctness guarantees.