All projects

Standalone Lean project

ExistentialRules

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.

Repository catalogLean 4.32.0Apache-2.0Repository

Repository catalog

Exact declarations are not indexed yet

Therefore has checked the project identity, repository, toolchain, and license metadata shown here. Proof-level source will appear only after a pinned ingestion records declarations, source ranges, and revisions.

Inspect the repository