A formalisation of the myhill-nerode theorem based on regular expressions
- Submitting institution
-
King's College London
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 87464783
- Type
- D - Journal article
- DOI
-
10.1007/s10817-013-9297-2
- Title of journal
- JOURNAL OF AUTOMATED REASONING
- Article number
- -
- First page
- 451
- Volume
- 52
- Issue
- 4
- ISSN
- 0168-7433
- Open access status
- Out of scope for open access requirements
- Month of publication
- January
- Year of publication
- 2014
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
-
- Citation count
- 9
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper provides the first formalisation of the Myhill-Nerode theorem which uses only regular expressions. Several other formalisations exist, but they use automata, which are difficult to reason about in theorem provers. By using regular expressions, the paper solves a longstanding problem of how to define regular languages in HOL-based theorem provers. This work has led to follow-up work in Coq, Matita and HOL4 theorem provers. It also establishes the fact that complement regular languages can be constructed without the complementation of automata.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -