@techreport{calcagno2003deciding,
author = {Calcagno, Cristiano and Cardelli, Luca and Gordon, Andy},
title = {Deciding Validity in a Spatial Logic for Trees},
institution = {Microsoft},
year = {2003},
month = {January},
abstract = {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.},
url = {http://approjects.co.za/?big=en-us/research/publication/deciding-validity-in-a-spatial-logic-for-trees-2003/},
number = {MSR-TR-2002-113},
note = {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.},
}