Deciding Validity in a Spatial Logic for Trees - Calcagno, Cristiano; Cardelli, Luca; Gordon, Andy (Microsoft, 2003)
We consider a propositional spatial logic for finite trees. The logic includes A|B (tree composition), A|> B (the implication induced by composition), and 0 (the unit of composition). We show that the satisfaction and validity problems are equivalent, and decidable. The crux of the argument is devising a finite enumeration of trees to consider when deciding whether a spatial implication is satisfied. We introduce a sequent calculus for the logic, and show it to be sound and complete with respect to an interpretation in terms of satisfaction. Finally, we describe a complete proof procedure for the sequent calculus. We envisage applications in the area of logic-based type systems for semistructured data. We describe a small programming language based on this idea.
A portion of this work appears in the proceedings of the ACM SIGPLAN Workshop on Types in Language Design and Implementation, New Orleans, January 18, 2003.