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

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

cs.AIApr 2, 2026

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

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

Organizations: LTCI, LaHDAK · Telecom Paris, Institut Polytechnique de Paris, France · Université Paris-Saclay, France · ENS de Lyon ·

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.

Figures & tables

	Truth	Formula	Context	Semi-
	Representation	Quantif	Quantif	decidable
Moore,1981	yes	yes	NA	yes
Genesereth,1991	yes	yes	yes	no
Halpern & Moses,1992	yes	no	no	yes
McCarthy,1993	yes	no	no	NA
Giunchiglia,1997	NA	no	no	NA

Table 1. Semi-decidability and the desiderata of Truth Representation, Formula Quantification, and Context Quantification

Panel of Figure 1 — Figure 1. Inclusion relationship ( $\hookrightarrow$ ) between subsets of the set of terms $\mathcal{T}$ and subset $\mathcal{L}_{q}$ of $\mathcal{L}$ .

Panel of Figure 2 — 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.

Event Calculus operator	Description
0	The first time instant
$i_{1}<i_{2}$	Instant $i_{1}$ occurs before instant $i_{2}$
$\textit{Initially}(\underline{\smash{\varphi}})$	Nontemporal quoted formula $\underline{\smash{\varphi}}$ holds at the beginning
$\textit{HoldsAt}(\underline{\smash{\varphi}},i_{1})$	Nontemporal quoted formula $\underline{\smash{\varphi}}$ holds at time $i_{1}$
$\textit{Happens}(a,i_{1},i_{2})$	Action $a$ happens between times $i_{1}$ and $i_{2}$
$\textit{Initiates}(a,\underline{\smash{\varphi}},i_{1})$	If action occurs at time $i_{1}$ it initiates $\underline{\smash{\varphi}}$ at that time

Table 2. Matching Event Calculus operators to their descriptions

Type	Name	Description
$o$	Objects	Non-Qiana objects (people, places, …)
$q$	Quotations	Type of all quotations (quoted formulas, quoted terms, …)
$c$	Contexts	Contexts
$\tau$	Time instant	Event calculus points in time.
$a$	Actions	Event calculus actions

Table 3. Types and their descriptions in Qiana

Logical Reasoning

Logical reasoning studies how formal rules support valid inference, knowledge representation, and reliable decisions.

See all 160 papers

First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)
Jul 12, 2026Christoph Benzmüller, Daniel KirchnerAutomated Theorem Proving Interactive Theorem Proving
University of Bamberg, Bamberg, Germany · Freie Universität Berlin, Berlin, Germany
The Dynamic Turn in Paraconsistency
Jul 22, 2026Rafael Ongaratto, Hans van DitmarschLogical Reasoning Dynamic Epistemic Logic
Institute of Philosophy and Human Sciences, UNICAMP Campinas, Brazil · University of Toulouse, IRIT-CNRS Toulouse, France
Applications of Intuitionistic Temporal Logic to Temporal Answer Set Programming
Mar 16, 2026Pedro Cabalar, Martín Diéguez, David Fernández-Duque +3Answer Set Programming Temporal Reasoning
University of Corunna, Spain · University of Angers, France · University of Barcelona, Spain +2

Jul 12, 2026J/K move · Enter open · S save

First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)

Christoph Benzmüller, Daniel Kirchner

University of Bamberg, Bamberg, Germany · Freie Universität Berlin, Berlin, Germany

Automated Theorem Proving Interactive Theorem Proving

Open paper AskPDF arXiv

We extend, in Isabelle/HOL, the deep-and-shallow embedding methodology of our prior work from propositional to first-order modal logic (FML) with constant-domain Kripke semantics. Three embeddings of FML into classical higher-order logic (HOL) are provided side by side: a deep embedding, a heavyweight maximal-shallow embedding, and a lightweight minimal-shallow embedding. The minimal-shallow embedding is presented as an Isabelle/HOL locale, parametrised by an accessibility relation, a world-indexed interpretation, a universe of worlds, and a variable assignment; the locale form admits a global faithfulness theorem, stating that quantifying over all minimal-shallow interpretations recovers exactly deep validity. A central technical contribution is a mechanisation, for FML under constant-domain Kripke semantics, of the (countable) downward Löwenheim-Skolem theorem, which underpins the automation of our faithfulness proof between the deep and minimal-shallow embeddings. Deploying it inside an extension of the minimal-shallow locale resolves the surjectivity problem that arises against an uncountable domain of individuals -- where the locale's variable assignment, having countable domain V = nat, cannot be surjective onto the domain -- and thereby yields faithfulness over the full domain. Since prior work treats only the propositional fragment, we develop here the substitution machinery (free/bound-variable predicates, the fresh-variable function, capture-avoiding substitution, alphabetic renaming, the substitutability predicate, the substitution lemma, and size-based induction principles) needed for the first-order quantifiers.

Abstract

Logical Reasoning

Explore similar work

First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)

The Dynamic Turn in Paraconsistency

Applications of Intuitionistic Temporal Logic to Temporal Answer Set Programming