English

Binary intersection formalized

Formal Languages and Automata Theory 2022-03-15 v1 Artificial Intelligence

Abstract

We provide a reformulation and a formalization of the classical result by Juhani Karhum\"aki characterizing intersections of two languages of the form {x,y}{u,v}\{x,y\}^*\cap \{u,v\}^*. 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.

Cite

@article{arxiv.2006.16711,
  title  = {Binary intersection formalized},
  author = {Štěpán Holub and Štěpán Starosta},
  journal= {arXiv preprint arXiv:2006.16711},
  year   = {2022}
}
R2 v1 2026-06-23T16:43:55.333Z