Email Gateway (Aug 22 2022 at 10:01): Email Gateway (Aug 22 2022 at 10:01):From: Tobias Nipkow <nipkow@in.tum.de>
Dmitriy Traytel
We formalize new decision procedures for WS1S, M2L(Str), and Presburger
Arithmetics. Formulas of these logics denote regular languages. Unlike
traditional decision procedures, we do not translate formulas into automata
(nor into regular expressions), at least not explicitly. Instead we devise
notions of derivatives (inspired by Brzozowski derivatives for regular
expressions) that operate on formulas directly and compute a syntactic
bisimulation using these derivatives. The treatment of Boolean connectives and
quantifiers is uniform for all mentioned logics and is abstracted into a locale.
This locale is then instantiated by different atomic formulas and their
derivatives (which may differ even for the same logic under different encodings
of interpretations as formal words).
The WS1S instance is described in the draft paper "A Coalgebraic Decision
Procedure for WS1S"
(http://www21.in.tum.de/~traytel/papers/ws1s_derivatives/index.html) by the author.
http://afp.sourceforge.net/entries/Formula_Derivatives.shtml
Enjoy!
smime.p7s
Last updated: Nov 04 2025 at 01:44 UTC