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 :
Reports
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00071562
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 5:57:22 PM
Last modification on : Wednesday, December 18, 2019 - 5:33:23 PM
Long-term archiving on: Tuesday, February 22, 2011 - 11:57:40 AM

Identifiers

  • HAL Id : inria-00071562, version 1

Citation

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

Share

Metrics

Record views

265

Files downloads

232