Table of Contents
Fetching ...

Paraconsistent logic and query answering in inconsistent databases

C. A. Middelburg

TL;DR

A sequent calculus proof system is presented instead because such proof systems are generally considered more suitable as the basis of proof search procedures than natural deduction proof systems and proof search procedures can serve as the core of algorithms for computing consistent answers to queries.

Abstract

This paper concerns the paraconsistent logic LPQ$^{\supset,\mathsf{F}}$ and an application of it in the area of relational database theory. The notions of a relational database, a query applicable to a relational database, and a consistent answer to a query with respect to a possibly inconsistent relational database are considered from the perspective of this logic. This perspective enables among other things the definition of a consistent answer to a query with respect to a possibly inconsistent database without resort to database repairs. In a previous paper, LPQ$^{\supset,\mathsf{F}}$ is presented with a sequent-style natural deduction proof system. In this paper, a sequent calculus proof system is presented because it is common to use a sequent calculus proof system as the basis of proof search procedures and such procedures may form the core of algorithms for computing consistent answers to queries.

Paraconsistent logic and query answering in inconsistent databases

TL;DR

A sequent calculus proof system is presented instead because such proof systems are generally considered more suitable as the basis of proof search procedures than natural deduction proof systems and proof search procedures can serve as the core of algorithms for computing consistent answers to queries.

Abstract

This paper concerns the paraconsistent logic LPQ and an application of it in the area of relational database theory. The notions of a relational database, a query applicable to a relational database, and a consistent answer to a query with respect to a possibly inconsistent relational database are considered from the perspective of this logic. This perspective enables among other things the definition of a consistent answer to a query with respect to a possibly inconsistent database without resort to database repairs. In a previous paper, LPQ is presented with a sequent-style natural deduction proof system. In this paper, a sequent calculus proof system is presented because it is common to use a sequent calculus proof system as the basis of proof search procedures and such procedures may form the core of algorithms for computing consistent answers to queries.
Paper Structure (9 sections, 6 theorems, 8 equations, 2 tables)

This paper contains 9 sections, 6 theorems, 8 equations, 2 tables.

Key Result

theorem thmcountertheorem

Let $\mathbf{A}$ be a structure of $\mathrm{LPQ}^{ \mathbin{\supset},{\mathsf{F}}}(\Sigma)$ such that $\mathcal{U}\sp\mathbf{A}$ is finite, and let $\alpha$ be an assignment in $\mathbf{A}$. Then, for all $A \in \mathcal{F}(\Sigma)$, $[\space[ A ]\space]\sp{\mathbf{A}}\sb{\alpha} \in \{ \mathsf{t},

Theorems & Definitions (12)

  • theorem thmcountertheorem
  • proof
  • theorem thmcountertheorem
  • proof
  • theorem thmcountertheorem
  • proof
  • theorem thmcountertheorem
  • proof
  • theorem thmcountertheorem
  • proof
  • ...and 2 more