A Formalisation of Finite Automata using Hereditarily Finite Sets
International Conference on Automated Deduction
MetadataShow full item record
Paulson, L. (2015). A Formalisation of Finite Automata using Hereditarily Finite Sets. International Conference on Automated Deduction https://www.repository.cam.ac.uk/handle/1810/248317
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.
Embargo Lift Date
This record's URL: https://www.repository.cam.ac.uk/handle/1810/248317