We present a formalization of diagrammatic systems and transformations in a linear logic framework. We start by showing how to embed Constraint Multiset Grammars, a well-known method for the specification of diagram languages, into a fragment of linear logic in a provably sound and complete way. We then show how this same fragment can express several forms of visual transformations that are commonly used in reasoning with diagrams. By using formal logic as the basis of our framework we gain the significant advantage of an integrated treatment of syntactic and semantic features of diagram languages. Furthermore, since the logic fragment we are using is implemented in linear logic programming languages, the proposed framework is not only formally well-defined, but also allows the verification of the specification via direct execution
On a Uniform Logical Framework for Diagram Reasoning / Bottoni, Paolo Gaspare; B., Meyer; PARISI PRESICCE, Francesco. - STAMPA. - (2001), pp. 64-71. (Intervento presentato al convegno Human-Centric Computing Languages and Environments, 2001 tenutosi a Stresa nel 5-9/9/2001) [10.1109/HCC.2001.995240].
On a Uniform Logical Framework for Diagram Reasoning
BOTTONI, Paolo Gaspare;PARISI PRESICCE, Francesco
2001
Abstract
We present a formalization of diagrammatic systems and transformations in a linear logic framework. We start by showing how to embed Constraint Multiset Grammars, a well-known method for the specification of diagram languages, into a fragment of linear logic in a provably sound and complete way. We then show how this same fragment can express several forms of visual transformations that are commonly used in reasoning with diagrams. By using formal logic as the basis of our framework we gain the significant advantage of an integrated treatment of syntactic and semantic features of diagram languages. Furthermore, since the logic fragment we are using is implemented in linear logic programming languages, the proposed framework is not only formally well-defined, but also allows the verification of the specification via direct executionI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
