monsterkrampeExistentialRules0.2.0

This repo contains formalizations around Existential Rules (aka. Tuple-Generating Dependencies) with disjunctions and the Chase algorithm. Mostly this will be about (basics of) my own formal works.
Sort by
  1. Git dependency.
    Found on Reservoir.

    PossiblyInfiniteTrees4a9276e

    This repo formalizes (possibly) infinite trees of finite degree in Lean. So far this is mainly a dependency for one of my other projects and tailored towards this purpose. The repo features a formalization of (a special case of) König's Lemma.
  2. Git dependency.
    Not found on Reservoir.

    BasicLeanDatastructures359a19c