2026-07-25T01:58:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16724 2024-03-06T10:58:09Z ddc:004 open_access

A Verified Cyclicity Checker: For Theories with Overloaded Constants Gengelbach, Arve Åman Pohjola, Johannes cyclicity non-termination ad-hoc overloading definitions Isabelle/HOL Non-terminating (dependencies of) definitions can lead to logical contradictions, for example when defining a boolean constant as its own negation. Some proof assistants thus detect and disallow non-terminating definitions. Termination is generally undecidable when constants may have different definitions at different type instances, which is called (ad-hoc) overloading. The Isabelle/HOL proof assistant supports overloading of constant definitions, but relies on an unclear foundation for this critical termination check. With this paper we aim to close this gap: we present a mechanised proof that, for restricted overloading, non-terminating definitions are of a detectable cyclic shape, and we describe a mechanised algorithm with its correctness proof. In addition we demonstrate this cyclicity checker on parts of the Isabelle/HOL main library. Furthermore, we introduce the first-ever formally verified kernel of a proof assistant for higher-order logic with overloaded definitions. All our results are formalised in the HOL4 theorem prover. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Arve Gengelbach and Johannes Åman Pohjola 2022 Is Part Of LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2022.15 urn:nbn:de:0030-drops-167240 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.15 eng https://creativecommons.org/licenses/by/4.0/legalcode