Qiana: A First-Order Formalism to Quantify over Contexts and Formulas with Temporality
This work addresses the problem of formalizing contextual reasoning in logic for researchers in AI and formal methods, though it appears incremental as it builds on existing first-order logic foundations.
The authors introduced Qiana, a first-order logic framework for reasoning about formulas true only in specific contexts, enabling quantification over both formulas and contexts, supporting paraconsistent logics, and being finitely axiomatizable for compatibility with existing theorem provers.
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.