Helmut Seidl
Thomas Schwentick
ABSTRACT
A query against a database behind a site like Napster may search, e.g., for all users who have downloaded more jazz titles than pop music titles. In order to express such queries, we extend classical monadic second-order logic by Presburger predicates which pose numerical restrictions on the children (content) of an element node and provide a precise automata-theoretic characterization. While the existential fragment of the resulting logic is decidable, it turns out that satisfiability of the full logic is undecidable. Decidable satisfiability and a querying algorithm even with linear data complexity can be obtained if numerical constraints are only applied to those contents of elements where ordering is irrelevant. Finally, it is sketched how these techniques can be extended also to answer questions like, e.g., whether the total price of the jazz music downloaded so far exceeds a user's budget.
- A. Berlea and H. Seidl. Binary Queries. In Extreme Markup Languages 2002 Conference, Montreal, August 2002.]]Google Scholar
- L. Berman. The Complexity of Logical Theories. Theoretical Computer Science (TCS), 11:71--77, 1980.]]Google Scholar
- J.R. Büchi. Weak Second-order Arithmetic and Finite Automata. Math. Logik. Grund. Math., 6:66--92, 1960.]]Google ScholarCross Ref
- L. Cardelli and G. Ghelli. A Query Language Based on the Ambient Logic. In 10th European Symposium on Programming (ESOP), pages 1--22. LNCS 2028, Springer Verlag, 2001.]] Google ScholarDigital Library
- L. Cardelli and A. Gordon. Anytime, Anywhere: Modal Logics for Mobile Ambients. In 27th ACM Conf. on Principles of Programming Languages (POPL), pages 365--377, 2000.]] Google ScholarDigital Library
- G. Conforti, O. Ferrara, and G. Ghelli. TQL Algebra and its Implementation (Extended Abstract). In IFIP Int. Conf. on Theoretical Computer Science (IFIP TCS), pages 422--434, 2002.]] Google ScholarDigital Library
- G. Conforti, G. Ghelli, A. Albano, D. Colazzo, P. Manghi, and C. Sartiani. The Query Language TQL. In 5th Int. Workshop on the Web and Databases (WebDB), 2002.]]Google Scholar
- J. Ferrante and C.W. Racko. The Computational Complexity of Logical Theories, volume 718 of Lecture Notes in Mathematics. Springer Verlag, 1979.]]Google ScholarCross Ref
- M.J. Fischer and M.O. Rabin. Superexponential Complexity of Presburger Arithmetic. In AMS Symp. on the Complexity of Computational Computational Processes. Vol. 7, pages 27--41, 1974.]]Google Scholar
- S. Ginsburg and E.H. Spanier. Bounded ALGOL-like Languages. Trans. Amer. Math. Soc., 113:333--368, 1964.]]Google ScholarCross Ref
- S. Ginsburg and E.H. Spanier. Semigroups, Presburger Formulas and Languages. Pacific Journal of Mathematics, 16(2):285--296, 1966.]]Google ScholarCross Ref
- G. Gottlob and C. Koch. Monadic Datalog and the Expressive Power of Languages for Web Information Extraction. In PODS 2001, pages 17--28, 2002.]] Google ScholarDigital Library
- F. Klaedtke and H. Ruess. Parikh automata and monadic second-order logics with linear cardinality constraints. Technical Report 177, Institute of Computer Science at Freiburg University, 2002.]]Google Scholar
- O. Kupferman, U. Sattler, and M.Y. Vardi. The Complexity of the Graded μ-Calculus. In 18th Int. Conf. on Automated Deduction (CADE), pages 423--437. LNCS 2392, Springer Verlag, 2002.]] Google ScholarDigital Library
- D. Lugiez. A Good Class of Automata and Application to Inductive Theorem Proving. In 25th Int. Coll. on Automata, Languages and Programming (ICALP), pages 409--420. LNCS 1443, Springer Verlag, 1998.]] Google ScholarDigital Library
- D. Lugiez and S. Dal Zilio. Multitrees Automata, Presburger's Constraints and Tree Logics. Technical Report 08-2002, Laboratoire d'Informatique Fondamentale de Marseille, 2002.]]Google Scholar
- D. Lugiez and S. Dal Zilio. XML Schema, Tree Logic and Sheaves Automata. Technical Report RR-4631, INRIA, 2002.]]Google Scholar
- T. Milo, D. Suciu, and V. Vianu. Typechecking for XML Transformers. In Proceedings of the ACM Symposium on Principles of Database Systems, pages 11--22, Dallas, TX, 2000.]] Google ScholarDigital Library
- M. Minsky. Recursive Unsolvability of Post's Problem of Tag and Other Topics in the Theory of Turing Machines. Ann. of Math., 74:437--455, 1961.]]Google ScholarCross Ref
- A. Neumann and H. Seidl. Locating Matches of Tree Patterns in Forests. In V. Arvind and R. Ramanujam, editors, Foundations of Software Technology and Theoretical Computer Science (FSTTCS), LNCS, pages 134--145. Springer Verlag, 1998.]] Google ScholarDigital Library
- F. Neven and T. Schwentick. Query Automata over Finite Trees. Theoretical Computer Science (TCS), 275(1--2):633--674, 2002.]] Google ScholarDigital Library
- F. Neven, T. Schwentick, and V. Vianu. Towards Regular Languages over In nite Alphabets. In MFCS 2001, pages 560--572, 2001.]] Google ScholarDigital Library
- F. Neven and J. Van den Bussche. Expressiveness of Structured Document Query Languages Based on Attribute Grammars. Journal of the ACM, 49(1):56--100, 2002.]] Google ScholarDigital Library
- J. Niehren and A. Podelski. Feature Automata and Recognizable Sets of Feature Trees. In 4th Int. Conf. on Theory and Practice of Software Development (TAPSOFT), pages 356--375. LNCS 668, Springer Verlag, 1993.]] Google ScholarDigital Library
- H. Ohsaki. Beyond Regularity: Equational Tree Automata for Associative and Commutative Theories. In 15th Computer Science Logic (CSL), pages 539--553. LNCS 2142, Springer Verlag, 2001.]] Google ScholarDigital Library
- H. Ohsaki and T. Takai. Decidability and Closure Properties of Equational Tree Languages. In 13th Int. Conf. on Rewriting Techniques and Applications (RTA), pages 114--128. LNCS 2378, Springer Verlag, 2002.]] Google ScholarDigital Library
- R. Parikh. On Context-Free Languages. Journal of the ACM (JACM), 13(4):570--581, 1966.]] Google ScholarDigital Library
- P. Wolper and B. Boigelot. On the Construction of Automata from Linear Arithmetic Constraints. In Tools and Algorithms for Construction and Analysis of Systems, 6th Ann. Conf. (TACAS), pages 1--19. LNCS 1785, Springer Verlag, 2000.]] Google ScholarDigital Library
Index Terms
- Numerical document queries
Recommendations
How unprovable is Rabin's decidability theorem?
LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer ScienceWe study the strength of set-theoretic axioms needed to prove Rabin's theorem on the decidability of the MSO theory of the infinite binary tree. We first show that over the second-order arithmetic theory ACA0, the complementation theorem for ...
Expressiveness of structured document query languages based on attribute grammars
Structured document databases can be naturally viewed as derivation trees of a context-free grammar. Under this view, the classical formalism of attribute grammars becomes a formalism for structured document query languages. From this perspective, we ...
Arithmetic, first-order logic, and counting quantifiers
This article gives a thorough overview of what is known about first-order logic with counting quantifiers and with arithmetic predicates. As a main theorem we show that Presburger arithmetic is closed under unary counting quantifiers. Precisely, this ...
Comments