A formalisation of finite automata using hereditarily finite sets

DOI10.1007/978-3-319-21401-6_15zbMATH Open1465.68165arXiv1505.01662OpenAlexW1687114231MaRDI QIDQ3454094FDOQ3454094

Authors: Lawrence C. Paulson 

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1505.01662

Recommendations

• Finitary set theory
• scientific article; zbMATH DE number 7204453
• Hereditarily finite sets in constructive type theory
• Computer proofs about finite and regular sets: The unifying concept of subvariance.
• A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mechanization of proofs and logical operations (03B35) Other classical set theory (including functions, relations, and set algebra) (03E20)

Cites Work

• A formalisation of the Myhill-Nerode theorem based on regular expressions
• Unified decision procedures for regular expression equivalence
• Title not available (Why is that?)
• Locales: a module system for mathematical theories
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• Finite sets and Gödel's incompleteness theorems
• Title not available (Why is that?)
• Deciding Kleene algebras in \texttt{Coq}
• Proof Pearl: regular expression equivalence and relation algebra
• A constructive theory of regular languages in Coq
• Defining functions on equivalence classes

Cited In (8)

• Graph theory in Coq: minors, treewidth, and isomorphisms
• Computer proofs about finite and regular sets: The unifying concept of subvariance.
• A Verified Compositional Algorithm for AI Planning
• Formally verified algorithms for upper-bounding state space diameters
• Regular language representations in the constructive type theory of Coq
• Hereditarily Finite Sets
• Hereditarily finite sets in constructive type theory
• Two-Way Automata in Coq

Uses Software

• Locales
• Finite Automata HF

This page was built for publication: A formalisation of finite automata using hereditarily finite sets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3454094)