HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

A Logic You Can Count On

Silvano Dal Zilio 1 Denis Lugiez Charles Meyssonnier
1 MIMOSA - Migration and mobility : semantics and applications
CRISAM - Inria Sophia Antipolis - Méditerranée , Université de Provence - Aix-Marseille 1, MINES ParisTech - École nationale supérieure des mines de Paris
Abstract : 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.
Document type :
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 5:57:22 PM
Last modification on : Friday, February 4, 2022 - 3:19:54 AM
Long-term archiving on: : Tuesday, February 22, 2011 - 11:57:40 AM


  • HAL Id : inria-00071562, version 1


Silvano Dal Zilio, Denis Lugiez, Charles Meyssonnier. A Logic You Can Count On. RR-5022, INRIA. 2003. ⟨inria-00071562⟩



Record views


Files downloads