Reseña: A formalisation of finite automata using hereditarily finite sets

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre teoría de conjuntos titulado A formalisation of finite automata using hereditarily finite sets

Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).

Su resumen es

Hereditarily finite (HF) set theory provides a standard universe of sets, but with no infinite sets. Its utility is demonstrated through a formalisation of the theory of regular languages and finite automata, including the Myhill-Nerode theorem and Brzozowski’s minimisation algorithm. The states of an automaton are HF sets, possibly constructed by product, sum, powerset and similar operations.

El código de las correspondientes teorías en Isabelle se encuentra aquí.