TL;DR
This paper reformulates and formalizes a classical language intersection theorem using morphisms and proof assistant Isabelle/HOL, enhancing clarity and rigor in formal language theory.
Contribution
It introduces a new formalization of Karhumäki's intersection theorem using morphisms and Isabelle/HOL, providing a clearer and more rigorous presentation.
Findings
Formalization of the intersection theorem in Isabelle/HOL
Simplified and transparent formulation using morphisms
Enhanced rigor in formal language theory proofs
Abstract
We provide a reformulation and a formalization of the classical result by Juhani Karhum\"aki characterizing intersections of two languages of the form . We use the terminology of morphisms which allows to formulate the result in a shorter and more transparent way, and we formalize the result in the proof assistant Isabelle/HOL.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
