Existential Rules in Lean

This is a collection of some definitions, results, and proofs around Existential Rules (aka. Tuple-Generating Dependencies) with disjunctions and the Chase algorithm written up in LEAN 4. Mostly, the formalizations are related to my own research.

Broadly speaking, the chase takes a set of rules and an initial set of facts (called database) and computes further facts to satisfy all the rules in the most general way. This might require infinitely many "chase steps". In the presence of disjunctions, the chase is branching out to produce a set of fact sets to capture all "possible worlds".

More specifically, this repo contains a generalized formalization of the chase on disjunctive existential rules in ExistentialRules/ChaseSequence. The definition captures both the Skolem and restricted chase at the same time through a generic ObsoletenessCondition. The definition of the chase for disjunctive rules involves (possibly) infinite trees of finite degree formalized here.

Key results that are already formalized include the following:

• The result of the chase is a universal model set. That is, (1) each fact set in the result indeed satisfies all rules and (2) for any given model M of the rule set and the database, we can find a fact set in the chase result that can be homomorphically embedded into M.
• A chase sequence without alternative matches on rules without disjunctions yields a universal model that is a core. (Section 3 of this paper)
• If a rule set is model-faithful acyclic (MFA), then every chase sequence on every database terminates. (The formalization is inspired by Section 3.1 in this paper; MFA was originally introduced here.)
• A generalization of MFA that takes the obsoleteness condition into account. This in principle generalizes both Disjunctive MFA (DMFA) and Restricted MFA (RMFA). Also our formalization adds support for constants in rules, which are not allowed in the original definitions. The only catch is that the original notions are specialized to handle only "Datalog-first" chase sequences. Since we consider arbitrary chase sequences here right now, the formalized versions are, strictly speaking, incomparable to the ones from the papers. In the future, we plan to fill this gap by formalizing Datalog-first chase sequences and the more specialized versions of DMFA and RMFA. (For DMFA see Section 3.2 in this paper. For RMFA see Section 4 of this paper. DMFA and RMFA are essentially the same except for the difference in obsoleteness due to the different chase variants.)

Notes on Setup

Using elan / lake:

• Install elan, e.g. via nix-shell -p elan or simply nix develop if you are using nix.
• Run lake build to build the project. If the build is successful, the proofs are correct 🎉