# Connecting Proof Theory and Knowledge Representation: Sequent Calculi and the Chase with Existential Rules

arXiv: https://arxiv.org/abs/2306.02521 · HTML: https://mlsanity.com/paper/2306.02521/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 28 references that are in the map.
- First posted on arXiv 5 Jun 2023.

## Builds on (most cited first, 4 of 4)

- [Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents](https://mlsanity.com/paper/1910.05215/) (2019)
- [Finite-Cliquewidth Sets of Existential Rules: Toward a General Criterion for Decidable yet Highly Expressive Querying](https://mlsanity.com/paper/2209.02464/) (2022)
- [Automating Reasoning with Standpoint Logic via Nested Sequents](https://mlsanity.com/paper/2205.02749/) (2022)
- [Uniform and Modular Sequent Systems for Description Logics](https://mlsanity.com/paper/2206.09020/) (2022)

## Abstract (arXiv)

Chase algorithms are indispensable in the domain of knowledge base querying, which enable the extraction of implicit knowledge from a given database via applications of rules from a given ontology. Such algorithms have proved beneficial in identifying logical languages which admit decidable query entailment. Within the discipline of proof theory, sequent calculi have been used to write and design proof-search algorithms to identify decidable classes of logics. In this paper, we show that the chase mechanism in the context of existential rules is in essence the same as proof-search in an extension of Gentzen's sequent calculus for first-order logic. Moreover, we show that proof-search generates universal models of knowledge bases, a feature also exhibited by the chase. Thus, we formally connect a central tool for establishing decidability proof-theoretically with a central decidability tool in the context of knowledge representation.