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 条
  • [41] A finite first-order presentation of set theory
    Vaillant, S
    TYPES FOR PROOFS AND PROGRAMS, 2002, 2646 : 316 - 330
  • [42] FIRST-ORDER CHARACTERIZATION OF THE RADICAL OF A FINITE GROUP
    Wilson, John S.
    JOURNAL OF SYMBOLIC LOGIC, 2009, 74 (04) : 1429 - 1435
  • [43] On first-order sentences without finite models
    Djordjevic, M
    JOURNAL OF SYMBOLIC LOGIC, 2004, 69 (02) : 329 - 339
  • [44] Expressive Completeness of Two-Variable First-Order Logic with Counting for First-Order Logic Queries on Rooted Unranked Trees
    Hellings, Jelle
    Gyssens, Marc
    Van den Bussche, Jan
    Van Gucht, Dirk
    2023 38TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, LICS, 2023,
  • [45] The role of decidability in first order separations over classes of finite structures
    Lindell, S
    Weinstein, S
    15TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2000, : 45 - 50
  • [46] Updating DL-Lite Ontologies Through First-Order Queries
    De Giacomo, Giuseppe
    Oriol, Xavier
    Rosati, Riccardo
    Savo, Domenico Fabio
    SEMANTIC WEB - ISWC 2016, PT I, 2016, 9981 : 167 - 183
  • [47] First-order and counting theories of ω-automatic structures
    Kuske, Dietrich
    Lohrey, Markus
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2006, 3921 : 322 - 336
  • [48] A DICHOTOMY FOR FIRST-ORDER REDUCTS OF UNARY STRUCTURES
    Bodirsky, Manuel
    Mottet, Antoine
    LOGICAL METHODS IN COMPUTER SCIENCE, 2018, 14 (02)
  • [49] On Fundamental Proof Structures in First-Order Optimization
    Goujaud, Baptiste
    Dieuleveut, Aymeric
    Taylor, Adrien
    2023 62ND IEEE CONFERENCE ON DECISION AND CONTROL, CDC, 2023, : 3023 - 3030
  • [50] First-order and counting theories of ω-automatic structures
    Kuske, Dietrich
    Lohrey, Markus
    JOURNAL OF SYMBOLIC LOGIC, 2008, 73 (01) : 129 - 150