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.

翻译：Chase算法在知识库查询领域不可或缺，它通过从给定本体中应用规则，从特定数据库中提取隐式知识。这类算法已被证明有助于识别允许可判定查询蕴含的逻辑语言。在证明论学科领域，前件演算被用于编写和设计证明搜索算法以识别可判定逻辑类。本文表明，存在规则上下文中的Chase机制本质上与Gentzen一阶逻辑前件演算扩展中的证明搜索是等价的。此外，我们还证明证明搜索能够生成知识库的通用模型，这一特性也由Chase算法所展现。因此，我们在证明论中用于建立可判定性的核心工具与知识表示背景下的关键可判定性工具之间建立了形式化关联。