2010/03/23 by Ph. Balbiani, Philippe Balbiani, R. Echahed +6
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Model-Driven Software Engineering Techniques #Natural Language Processing Techniques #Programming Languages (cs.PL) #Semantic Web and Ontologies #Symbolic Computation (cs.SC) #cs.LO #cs.PL #cs.SC
paper · pdf · doi:10.48550/arxiv.1003.4369
arxiv created 2010/03/23 · openalex publication_date 2010/03/23 · arxiv updated 2010/03/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We propose a modal logic tailored to describe graph transformations and discuss some of its properties. We focus on a particular class of graphs called termgraphs. They are first-order terms augmented with sharing and cycles. Termgraphs allow one to describe classical data-structures (possibly with pointers) such as doubly-linked lists, circular lists etc. We show how the proposed logic can faithfully describe (i) termgraphs as well as (ii) the application of a termgraph rewrite rule (i.e. matching and replacement) and (iii) the computation of normal forms with respect to a given rewrite system. We also show how the proposed logic, which is more expressive than propositional dynamic logic, can be used to specify shapes of classical data-structures (e.g. binary trees, circular lists etc.).