Thanks for that. I’ve just merged it and since you have a patch already not attempted to repair.
Cheers, Gerwin On 13.06.2014, at 6:27 pm, Dmitriy Traytel <tray...@in.tum.de<mailto:tray...@in.tum.de>> wrote: I'm following the suggestion of announcing who will fix a new AFP entry for the development version. Of course, I will take care of MSO_Regex_Equivalence once it is merged into the development branch. The patch is actually already prepared. Dmitriy -------- Original-Nachricht -------- Betreff: [isabelle] New AFP entry: Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions Datum: Thu, 12 Jun 2014 22:35:58 +0200 Von: Tobias Nipkow <nip...@in.tum.de><mailto:nip...@in.tum.de> An: Isabelle Users <isabelle-us...@cl.cam.ac.uk><mailto:isabelle-us...@cl.cam.ac.uk> Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions Dmitriy Traytel and Tobias Nipkow Monadic second-order logic on finite words (MSO) is a decidable yet expressive logic into which many decision problems can be encoded. Since MSO formulas correspond to regular languages, equivalence of MSO formulas can be reduced to the equivalence of some regular structures (e.g. automata). We verify an executable decision procedure for MSO formulas that is not based on automata but on regular expressions. Decision procedures for regular expression equivalence have been formalized before, usually based on Brzozowski derivatives. Yet, for a straightforward embedding of MSO formulas into regular expressions an extension of regular expressions with a projection operation is required. We prove total correctness and completeness of an equivalence checker for regular expressions extended in that way. We also define a language-preserving translation of formulas into regular expressions with respect to two different semantics of MSO. The formalization is described in this ICFP 2013 functional pearl: http://www21.in.tum.de/~nipkow/pubs/icfp13.html http://afp.sourceforge.net/entries/MSO_Regex_Equivalence.shtml Enjoy! _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de<mailto:isabelle-...@in.tum.de> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
