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.