In this paper we investigate a new approach to formalizing interpretation of and reasoning with visual languages based on linear logic. We argue that an approach based on logic makes it possible to deal with different computational tasks in the usage of visual notations, from parsing and animation to reasoning about diagrams. However, classical first order logic, being monotonic, is not a suitable basis for such an approach. The paper therefore explores linear logic as an alternative. We demonstrate how parsing corresponds to linear proofs and prove the soundness and correctness of this mapping. As our mapping of grammars is into a subset of a linear logic programming language, we also demonstrate how multi-dimensional parsing can be understood as automated linear deduction. We proceed to discuss how the same framework can be used as the foundation of more complex forms of reasoning with and about diagrams.
A Static Analysis Method for a Classical Linear Logic Programming Language
