A Note on Proofs of Earley’s Recognizer

Tobias Nipkow, Martin Rau

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

Abstract

This paper presents the formalization and verification (in the proof assistant Isabelle) of an abstract inductive version of Earley’s recognizer, relates it to the standard definition and derives an efficient one-pass algorithm for ε-free grammars. In particular it compares Jones development of Earley’s recognizer to our own and to the literature.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Science and Business Media Deutschland GmbH
Pages45-55
Number of pages11
DOIs
StatePublished - 2024

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
VolumeLNCS 14781
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'A Note on Proofs of Earley’s Recognizer'. Together they form a unique fingerprint.

Cite this