Top

Published in:

2015 | OriginalPaper | Chapter

A Formalisation of Finite Automata Using Hereditarily Finite Sets

Author : Lawrence C. Paulson

Published in: Automated Deduction - CADE-25

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Deciding Satisfiability by Tableaux

next chapter SEPIA: Search for Proofs Using Inferred Automata

denotes a typed universal set, here the set of all words.

Ballarin, C.: Locales: A module system for mathematical theories. J. Autom. Reasoning 52(2), 123–153 (2014)MathSciNetCrossRef

Braibant, T., Pous, D.: Deciding Kleene algebras in Coq. Log. Methods Comput. Sci. 8(1), 1–42 (2012)MathSciNetCrossRef

Champarnaud, J., Khorsi, A., Paranthoën, T.: Split and join for minimizing: Brzozowski’s algorithm. In: Balík, M., Simánek, M. (eds.) The Prague Stringology Conference, pp. 96–104. Czech Technical University, Department of Computer Science and Engineering (2002)

Constable, R.L., Jackson, P.B., Naumov, P., Uribe, J.C.: Constructively formalizing automata theory. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction, pp. 213–238. MIT Press (2000)

Doczkal, C., Kaiser, J.-O., Smolka, G.: A constructive theory of regular languages in Coq. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 82–97. Springer, Heidelberg (2013) CrossRef

Hopcroft, J.E., Ullman, J.D.: Formal Languages and Their Relation to Automata. Addison-Wesley, Boston (1969)

Kozen, D.: Automata and computability. Springer, New York (1997) CrossRefMATH

Krauss, A., Nipkow, T.: Proof pearl: regular expression equivalence and relation algebra. J. Autom. Reasoning 49(1), 95–106 (2012)MathSciNetCrossRefMATH

Nipkow, T.: Verified lexical analysis. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 1–15. Springer, Heidelberg (1998) CrossRef

10.

Nipkow, T., Traytel, D.: Unified decision procedures for regular expression equivalence. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 450–466. Springer, Heidelberg (2014)

11.

Paulson, L.C.: Defining functions on equivalence classes. ACM Trans. Comput. Logic 7(4), 658–675 (2006)MathSciNetCrossRef

12.

Paulson, L.C.: Finite automata in hereditarily finite set theory. Archive of Formal Proofs, February 2015. http://afp.sf.net/entries/Finite_Automata_HF.shtml, Formal proof development

13.

Paulson, L.C.: A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. J. Autom. Reasoning 55(1), 1–37 (2015). Available online at http://link.springer.com/article/10.1007%2Fs10817-015-9322-8

14.

Świerczkowski, S.: Finite sets and Gödel’s incompleteness theorems. Dissertationes Mathematicae 422, 1–58 (2003). http://journals.impan.gov.pl/dm/Inf/422-0-1.html

15.

Wu, C., Zhang, X., Urban, C.: A formalisation of the Myhill-Nerode theorem based on regular expressions. J. Autom. Reasoning 52(4), 451–480 (2014)MathSciNetCrossRef

Title: A Formalisation of Finite Automata Using Hereditarily Finite Sets
Author: Lawrence C. Paulson
Publisher: Springer International Publishing
Book: Automated Deduction - CADE-25
Print ISBN: 978-3-319-21400-9

Electronic ISBN: 978-3-319-21401-6

Copyright Year: 2015
DOI: https://doi.org/10.1007/978-3-319-21401-6_15

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner