A logic you can count on

11 years 4 months ago
A logic you can count on
We prove the decidability of the quantifier-free, static fragment of ambient logic, with composition adjunct and iteration, which corresponds to a kind of regular expression language for semistructured data. The essence of this result is a surprising connection between formulas of the ambient logic and counting constraints on (nested) vectors of integers. Our proof method is based on a new class of tree automata for unranked, unordered trees, which may result in practical algorithms for deciding the satisfiability of a formula. A benefit of our approach is to naturally lead to an extension of the logic with recursive definitions, which is also decidable. Finally, we identify a simple syntactic restriction on formulas that improves the effectiveness of our algorithms on large examples. Categories and Subject Descriptors: E.1 [Data Structures]: Trees; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic--modal logic; F.4.3 [Mathematical Logic and Formal Languages]: Formal...
Silvano Dal-Zilio, Denis Lugiez, Charles Meyssonni
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2004
Where POPL
Authors Silvano Dal-Zilio, Denis Lugiez, Charles Meyssonnier
Comments (0)