Search papers, labs, and topics across Lattice.
Qiana is introduced, a first-order logic framework enabling quantification over both formulas and the contexts in which they hold true. This allows for expressing complex relationships like universal knowledge within specific contexts and handling contradictions within those contexts via paraconsistent logics. The framework's basis in first-order logic ensures compatibility with existing theorem provers.
Finally, a first-order logic that lets you quantify over contexts and formulas, so you can reason about what's true *where*.
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.