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

TL;DR

Qiana is a first-order logic framework enabling reasoning over formulas and contexts with temporality, supporting contradictions and compatibility with existing theorem provers.

Contribution

It introduces a novel first-order formalism for quantifying over contexts and formulas, incorporating temporality and paraconsistency.

Findings

Qiana can represent temporality, event calculus, and modal logic.

It is finitely axiomatizable and compatible with existing first-order theorem provers.

Supports reasoning with contradictions within contexts.

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.