2026-07-22T00:13:43Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22785 2025-10-02T11:31:53Z ddc:004 open_access

Strong Induction Is an Up-To Technique Bonchi, Filippo Di Lavore, Elena Ricci, Anna Induction Coinduction Up-to Techniques Induction up-to Lattices Algebras Up-to techniques are enhancements of the coinduction proof principle which, in lattice theoretic terms, is the dual of induction. What is the dual of coinduction up-to? By means of duality, we illustrate a theory of induction up-to and we observe that an elementary proof technique, commonly known as strong induction, is an instance of induction up-to. We also show that, when generalising our theory from lattices to categories, one obtains an enhancement of the induction definition principle known in the literature as comonadic recursion. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Filippo Bonchi and Elena Di Lavore and Anna Ricci 2025 Is Part Of LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2025.28 urn:nbn:de:0030-drops-227856 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.28 eng https://creativecommons.org/licenses/by/4.0/legalcode