Search arXiv⌕ Search

arXiv · cs/0406013

Optimization of Bound Disjunctive Queries with Constraints

Abstract

"To Appear in Theory and Practice of Logic Programming (TPLP)" This paper presents a technique for the optimization of bound queries over disjunctive deductive databases with constraints. The proposed approach is an extension of the well-known Magic-Set technique and is well-suited for being integrated in current bottom-up (stable) model inference engines. More specifically, it is based on the exploitation of binding propagation techniques which reduce the size of the data relevant to answer the query and, consequently, reduces both the complexity of computing a single model and the number of models to be considered. The motivation of this work stems from the observation that traditional binding propagation optimization techniques for bottom-up model generator systems, simulating the goal driven evaluation of top-down engines, are only suitable for positive (disjunctive) queries, while hard problems are expressed using unstratified negation. The main contribution of the paper consists in the extension of a previous technique, defined for positive disjunctive queries, to queries containing both disjunctive heads and constraints (a simple and expressive form of unstratified negation). As the usual way of expressing declaratively hard problems is based on the guess-and-check technique, where the guess part is expressed by means of disjunctive rules and the check part is expressed by means of constraints, the technique proposed here is highly relevant for the optimization of queries expressing hard problems. The value of the technique has been proved by several experiments.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

G. Greco, S. Greco, I. Trubtsyna, E. Zumpano. 2004-06-07. Optimization of Bound Disjunctive Queries with Constraints. https://arxiv.org/abs/cs/0406013

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

A Deeper Look at Depth: Stable Generation Accounting for Quantifier Reasoning

SMT solvers make automated verification convenient. At the same time, solvers suffer from instability, whereby seemingly inconsequential changes to the input may cause a previously quickly produced proof to fail or time out. This paper addresses a common cause of outcome instability (i.e., unsat/unknown fluctuations) in the context of program verification. We demonstrate that the generation (i.e., depth) accounting used to make quantifier instantiation practical and implemented in multiple state-of-the-art SMT solvers is non-confluent (i.e., prone to divergence), and that this leads to instability. We then address this deficiency and develop a new accounting method that is stable. The new method is justified using a sequence of refinements from an abstract, confluent solver model all the way to our implementation in Z3. Our empirical evaluation demonstrates that our implementation reduces outcome instability by 94% in the unstable core of the Mariposa benchmark without leading to performance regressions.

cs.LO↗

Typed Knowledge over Constructive Institutions

Type theories designed for mathematics or program verification need only that a proposition holds; proof irrelevance in conversion erases, at the kernel level, how a claim was established. A persistent knowledge store, by contrast, must retain that record: who established a claim, by which derivation or external tool, and under which assumptions. This volume presents the theory of Eigenius---a store of typed knowledge over constructive institutions---and develops its metatheory from that requirement. The kernel theory is a dependent type theory with cumulative universes, an impredicative universe of propositions, inductive families, and an intensional identity type. Proof irrelevance is an axiom with an explicit witness rather than a conversion rule, so proofs of a proposition are provably equal yet remain distinct terms. Definitional equality is joinability under an orthogonal rewriting system---confluent, injective on type formers, and decidable by a type-free test---while a separate subsumption judgment covers universe cumulativity, codomain-covariant function types, and declared class inclusions. We prove consistency via a set-theoretic model; develop a justification logic over the kernel's propositions to track evidence and support; organize environments as an institution so that store extensions are signature morphisms and external verdicts enter via comorphisms; formulate a typed knowledge-graph theory with records, classes, and refinements; and prove the correctness of conversion, normalization by evaluation, and bidirectional type checking relative to termination. A Lean 4 formalization accompanies the volume.

cs.LO↗

A formal specification of the jq language

jq is a widely used tool that provides a programming language to manipulate JSON data. However, the jq language is currently only specified by its implementation, making it difficult to reason about its behaviour. To this end, we provide a formal syntax and denotational semantics for a large subset of the jq language. In particular, we give a translation from jq programs to lambda terms. Our most significant contribution is to provide a new way to interpret updates that allows for more performant execution. We implement our semantics in two interpreters and evaluate the performance.

cs.LO↗