{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T09:49:35Z","timestamp":1791020975471,"version":"4.1.0"},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2005,1,5]],"date-time":"2005-01-05T00:00:00Z","timestamp":1104883200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2005,7]]},"abstract":"<jats:p>\n                    We consider a propositional spatial logic for finite trees. The logic includes\n                    <jats:inline-formula>$\\A \\Par \\B$<\/jats:inline-formula>\n                    (tree composition),\n                    <jats:inline-formula>$\\A \\,{\\Guarantee}\\, \\B$<\/jats:inline-formula>\n                    (the implication induced by composition), and\n                    <jats:inline-formula>$\\Zero$<\/jats:inline-formula>\n                    (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.\n                  <\/jats:p>","DOI":"10.1017\/s0956796804005404","type":"journal-article","created":{"date-parts":[[2005,7,12]],"date-time":"2005-07-12T07:02:54Z","timestamp":1121151774000},"page":"543-572","source":"Crossref","is-referenced-by-count":17,"title":["Deciding validity in a spatial logic for trees"],"prefix":"10.1017","volume":"15","author":[{"given":"CRISTIANO","family":"CALCAGNO","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"LUCA","family":"CARDELLI","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ANDREW D.","family":"GORDON","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2005,1,5]]},"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796804005404","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:34:53Z","timestamp":1779834893000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796804005404\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1,5]]},"references-count":0,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,1]]}},"alternative-id":["S0956796804005404"],"URL":"https:\/\/doi.org\/10.1017\/s0956796804005404","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,1,5]]}}}