Safe extension of a logic with definitional axioms need acyclic definitions, because cycles in definitions possibly entail contradiction. In this report we give a mechanised exact characterisation of acyclic overloading definitions. Our results support the soundness argument of the cyclicity checker of the Isabelle/HOL theorem prover, and serve as the theoretical foundation for future verification of such a cyclicity checker.
Available as PDF (421 kB, no cover)
Download BibTeX entry.