Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Qiana: A First-Order Formalism to Quantify over Contexts and Formulas with Temporality

Simon Coumes, Pierre-Henri Paris, François Schwarzentruber, Fabian Suchanek

Abstract

We introduce Qiana, a logic framework for reasoning on formulas that are true only in specific contexts. In Qiana, it is possible to quantify over both formulas and contexts to express, e.g., that ``everyone knows everything Alice says''. Qiana also permits paraconsistent logics within contexts, so that contexts can contain contradictions. Furthermore, Qiana is based on first-order logic, and is finitely axiomatizable, so that Qiana theories are compatible with pre-existing first-order logic theorem provers. We show how Qiana can be used to represent temporality, event calculus, and modal logic. We also discuss different design alternatives of Qiana.

Qiana: A First-Order Formalism to Quantify over Contexts and Formulas with Temporality

Abstract

We introduce Qiana, a logic framework for reasoning on formulas that are true only in specific contexts. In Qiana, it is possible to quantify over both formulas and contexts to express, e.g., that ``everyone knows everything Alice says''. Qiana also permits paraconsistent logics within contexts, so that contexts can contain contradictions. Furthermore, Qiana is based on first-order logic, and is finitely axiomatizable, so that Qiana theories are compatible with pre-existing first-order logic theorem provers. We show how Qiana can be used to represent temporality, event calculus, and modal logic. We also discuss different design alternatives of Qiana.

Paper Structure

This paper contains 44 sections, 15 theorems, 115 equations, 2 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Notations
  4. Quoting and Unquoting Formulas
  5. Quotation Sets
  6. Quoting
  7. Substitution on Quotations
  8. Unquoting
  9. Defining Qiana
  10. Truth Axioms
  11. Axioms for Reasoning in Contexts
  12. Qiana
  13. Examples and Discussion
  14. Reasoning in Epistemic Contexts
  15. Paraconsistency
  16. ...and 29 more sections

Key Result

Proposition 1

$\mu$ is injective on $\mathcal{L}_q$. $\blacktriangleleft$$\blacktriangleleft$

Figures (2)

  • Figure 1: Inclusion relationship ($\hookrightarrow$) between subsets of the set of terms $\mathcal{T}$ and subset $\mathcal{L}_q$ of $\mathcal{L}$.
  • Figure 2: Overview of the process of finite axiomatization. Zizag arrows indicate the finite sets are counterparts to the top infinite ones. Dotted arrows indicate the the elements of $H_{\textit{tools}}^\textit{fin}$ are used to define said counterparts.

Theorems & Definitions (45)

  • Example 1
  • Definition 1: augmented signature
  • Definition 2
  • Remark 1
  • Example 2
  • Definition 3
  • Remark 2
  • Definition 4
  • Definition 5
  • Example 3
  • ...and 35 more