Standard
Unified Decision Procedures for Regular Expression Equivalence. / Nipkow, Tobias; Traytel, Dmitriy.
ITP 2014 - Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. red. / Gerwin Klein; Ruben Gamboa. Bind 8558 Springer, Cham, 2014. s. 450-466 (LNCS).
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
Nipkow, T
& Traytel, D 2014,
Unified Decision Procedures for Regular Expression Equivalence. i G Klein & R Gamboa (red),
ITP 2014 - Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. bind 8558, Springer, Cham, LNCS, s. 450-466.
https://doi.org/10.1007/978-3-319-08970-6_29APA
Nipkow, T.
, & Traytel, D. (2014).
Unified Decision Procedures for Regular Expression Equivalence. I G. Klein, & R. Gamboa (red.),
ITP 2014 - Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings (Bind 8558, s. 450-466). Springer, Cham. LNCS
https://doi.org/10.1007/978-3-319-08970-6_29Vancouver
Nipkow T
, Traytel D.
Unified Decision Procedures for Regular Expression Equivalence. I Klein G, Gamboa R, red., ITP 2014 - Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. Bind 8558. Springer, Cham. 2014. s. 450-466. (LNCS).
https://doi.org/10.1007/978-3-319-08970-6_29Author
Nipkow, Tobias ; Traytel, Dmitriy. / Unified Decision Procedures for Regular Expression Equivalence. ITP 2014 - Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. red. / Gerwin Klein ; Ruben Gamboa. Bind 8558 Springer, Cham, 2014. s. 450-466 (LNCS).
Bibtex
@inproceedings{9e5d7ac741dd47fd9868443cbcd57cb5,
title = "Unified Decision Procedures for Regular Expression Equivalence",
abstract = "We formalize a unified framework for verified decision procedures for regular expression equivalence. Five recently published formalizations of such decision procedures (three based on derivatives, two on marked regular expressions) can be obtained as instances of the framework. We discover that the two approaches based on marked regular expressions, which were previously thought to be the same, are different, and we prove a quotient relation between the automata produced by them. The common framework makes it possible to compare the performance of the different decision procedures in a meaningful way.",
author = "Tobias Nipkow and Dmitriy Traytel",
year = "2014",
doi = "10.1007/978-3-319-08970-6_29",
language = "English",
volume = "8558",
series = "LNCS",
pages = "450--466",
editor = "Gerwin Klein and Ruben Gamboa",
booktitle = "ITP 2014 - Interactive Theorem Proving",
publisher = "Springer, Cham",
}
RIS
TY - GEN
T1 - Unified Decision Procedures for Regular Expression Equivalence
AU - Nipkow, Tobias
AU - Traytel, Dmitriy
PY - 2014
Y1 - 2014
N2 - We formalize a unified framework for verified decision procedures for regular expression equivalence. Five recently published formalizations of such decision procedures (three based on derivatives, two on marked regular expressions) can be obtained as instances of the framework. We discover that the two approaches based on marked regular expressions, which were previously thought to be the same, are different, and we prove a quotient relation between the automata produced by them. The common framework makes it possible to compare the performance of the different decision procedures in a meaningful way.
AB - We formalize a unified framework for verified decision procedures for regular expression equivalence. Five recently published formalizations of such decision procedures (three based on derivatives, two on marked regular expressions) can be obtained as instances of the framework. We discover that the two approaches based on marked regular expressions, which were previously thought to be the same, are different, and we prove a quotient relation between the automata produced by them. The common framework makes it possible to compare the performance of the different decision procedures in a meaningful way.
U2 - 10.1007/978-3-319-08970-6_29
DO - 10.1007/978-3-319-08970-6_29
M3 - Article in proceedings
VL - 8558
T3 - LNCS
SP - 450
EP - 466
BT - ITP 2014 - Interactive Theorem Proving
A2 - Klein, Gerwin
A2 - Gamboa, Ruben
PB - Springer, Cham
ER -
