Title: Deciding validity in a spatial logic for trees
Abstract: (MATH) We consider a propositional spatial logic for finite trees. The logic includes A ???? Par B (tree composition), A ???? B (the implication induced by composition), and O (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.
Publication Year: 2003
Publication Date: 2003-01-18
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 53
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot