A Formalisation of Finite Automata Using Hereditarily Finite Sets

DOI10.1007/978-3-319-21401-6_15zbMath1465.68165arXiv1505.01662OpenAlexW1687114231MaRDI QIDQ3454094

Lawrence Charles 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)

Related Items (7)

Formally verified algorithms for upper-bounding state space diameters ⋮ Regular language representations in the constructive type theory of Coq ⋮ Graph theory in Coq: minors, treewidth, and isomorphisms ⋮ A Verified Compositional Algorithm for AI Planning ⋮ Hereditarily Finite Sets ⋮ Two-Way Automata in Coq ⋮ Hereditarily Finite Sets in Constructive Type Theory

Uses Software

• Locales
• Finite Automata HF

Cites Work

• Unnamed Item
• Unnamed Item
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• A formalisation of the Myhill-Nerode theorem based on regular expressions
• Locales: a module system for mathematical theories
• Proof Pearl: regular expression equivalence and relation algebra
• Unified Decision Procedures for Regular Expression Equivalence
• Deciding Kleene Algebras in Coq
• A Constructive Theory of Regular Languages in Coq
• Finite sets and Gödel's incompleteness theorems
• Defining functions on equivalence classes

This page was built for publication: A Formalisation of Finite Automata Using Hereditarily Finite Sets