A formalisation of finite automata using hereditarily finite sets

DOI10.1007/978-3-319-21401-6_15MaRDI QIDQ3454094zbMATH OpenOpenAlexFDO

Authors Lawrence C. Paulson

Publication date 2 December 2015

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

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

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)

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.

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)

Cites work

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

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
• Hereditarily Finite Sets
• Formally verified algorithms for upper-bounding state space diameters
• Regular language representations in the constructive type theory of Coq
• Hereditarily finite sets in constructive type theory
• Two-Way Automata in Coq

Describes a project that uses

Uses Software

• Finite Automata HF
• Locales

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)