Second-Order Specifications and Quantifier Elimination for Consistent Query Answering in Databases
Consistent answers to a query from a possibly inconsistent database are answers that are simultaneously retrieved from every possible repair of the database. Repairs are consistent instances that minimally differ from the original inconsistent instance. It has been shown before that database repairs can be specified as the stable models of a disjunctive logic program. In this paper we show how to use the repair programs to transform the problem of consistent query answering into a problem of reasoning w.r.t. a theory written in second-order predicate logic. It also investigated how a first-order theory can be obtained instead by applying second-order quantifier elimination techniques.
Code (0)
등록된 구현이 없습니다.
Methods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic
For relational monadic formulas (the L\"owenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, projection and forgetting - operations that currently receive …
Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof
In recent years, G\"odel's ontological proof and variations of it were formalized and analyzed with automated tools in various ways. We supplement these analyses with a modeling in an automated environment based on first…
Automated Theorem ProvingPIE -- Proving, Interpolating and Eliminating on the Basis of First-Order Logic
PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. It includes a versatile formula macro system and supports the creation of documents that intersperse macro definitions, reas…
Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic
PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. Its main focus is on formulas, as constituents of complex formalizations that are structured through formula macros, and as …
Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization
The problem of checking satisfiability of linear real arithmetic (LRA) and non-linear real arithmetic (NRA) formulas has broad applications, in particular, they are at the heart of logic-related applications such as logi…