A formalisation of finite automata using hereditarily finite sets

Paulson, Lawrence

View / Open Files

Paulson 2015 International Conference on Automated Deduction.pdf (PDF, 188Kb)

Authors

Paulson, Lawrence

Publication Date

2015

Journal Title

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ISSN

0302-9743

ISBN

978-3-319-21400-9

Publisher

Springer International Publishing

Language

English

Type

Conference Object

Metadata

Show full item record

Citation

Paulson, L. (2015). A formalisation of finite automata using hereditarily finite sets. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) https://doi.org/10.1007/978-3-319-21401-6_15

Abstract

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

2050-07-29

Identifiers

External DOI: https://doi.org/10.1007/978-3-319-21401-6_15

This record's URL: https://www.repository.cam.ac.uk/handle/1810/248317

Rights

Licence:

http://www.rioxx.net/licenses/all-rights-reserved