First-order queries on finite structures over the reals

被引:18
|
作者
Paredaens, J
Van den Bussche, J
Van Gucht, D
机构
[1] Univ Instelling Antwerp, Dept Math & Comp Sci, B-2610 Antwerp, Belgium
[2] Limburgs Univ Ctr, Dept WNI, B-3590 Diepenbeek, Belgium
[3] Indiana Univ, Dept Comp Sci, Bloomington, IN 47405 USA
关键词
first-order logic; linear arithmetic; relational databases; constraint programming;
D O I
10.1137/S009753979629766
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We investigate properties of finite relational structures over the reals expressed by first-order sentences whose predicates are the relations of the structure plus arbitrary polynomial inequalities, and whose quantifiers can range over the whole set of reals. In constraint programming terminology, this corresponds to Boolean real polynomial constraint queries on finite structures. The fact that quantifiers range over all reals seems crucial; however, we observe that each sentence in the first-order theory of the reals can be evaluated by letting each quantifier range over only a finite set of real numbers without changing its truth value. Inspired by this observation, we then show that when all polynomials used are linear, each query can be expressed uniformly on all finite structures by a sentence of which the quantifiers range only over the finite domain of the structure. In other words, linear constraint programming on finite structures can be reduced to ordinary query evaluation as usual in finite model theory and databases. Moreover, if only "generic" queries are taken into consideration, we show that this can be reduced even further by proving that such queries can be expressed by sentences using as polynomial inequalities only those of the simple form chi < y.
引用
收藏
页码:1747 / 1763
页数:17
相关论文
共 50 条
  • [1] Decomposition of decidable first-order logics over integers and reals
    Bouchy, Florent
    Finkel, Alain
    Leroux, Jerome
    TIME 2008: 15TH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2008, : 147 - +
  • [2] FIRST-ORDER QUERIES ON CLASSES OF STRUCTURES WITH BOUNDED EXPANSION
    Kazana, Wojciech
    Segoufin, Luc
    LOGICAL METHODS IN COMPUTER SCIENCE, 2020, 16 (01)
  • [3] Decidability of first-order logic queries over views
    Bailey, J
    Dong, GZ
    DATABASE THEORY - ICDT'99, 1999, 1540 : 83 - 99
  • [4] First-order queries over one unary function
    Durand, A.
    Olive, F.
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2006, 4207 : 334 - 348
  • [5] On the strictness of the first-order quantifier structure hierarchy over finite structures
    He, Yuguo
    25TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2010), 2010, : 170 - 178
  • [6] First-Order Orbit Queries
    Shaull Almagor
    Joël Ouaknine
    James Worrell
    Theory of Computing Systems, 2021, 65 : 638 - 661
  • [7] First-Order Orbit Queries
    Almagor, Shaull
    Ouaknine, Joel
    Worrell, James
    THEORY OF COMPUTING SYSTEMS, 2021, 65 (04) : 638 - 661
  • [8] On first-order topological queries
    Grohe, M
    Segoufin, L
    15TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2000, : 349 - 360
  • [9] First-order queries on structures of bounded degree are computable with constant delay
    Durand, Arnaud
    Grandjean, Etienne
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2007, 8 (04)
  • [10] ENUMERATING ANSWERS TO FIRST-ORDER QUERIES OVER DATABASES OF LOW DEGREE
    Durand, Arnaud
    Schweikardt, Nicole
    Segoufin, Luc
    LOGICAL METHODS IN COMPUTER SCIENCE, 2022, 18 (02)