### Abstract

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 by the author.

### License

BSD License

### Topics

- Computer science/Automata and formal languages
- Logic/General logic/Decidability of theories

### Session Formula_Derivatives

- While_Default
- FSet_More
- Automaton
- Abstract_Formula
- WS1S_Prelim
- WS1S_Formula
- WS1S_Alt_Formula
- Presburger_Formula
- WS1S_Presburger_Equivalence
- WS1S_Nameful

### Session Formula_Derivatives-Examples

- WS1S_Examples
- WS1S_Alt_Examples
- Presburger_Examples
- WS1S_Presburger_Examples
- WS1S_Nameful_Examples

### Depends on

- A Codatatype of Formal Languages
- Deriving class instances for datatypes
- List Index
- Haskell’s Show Class in Isabelle/HOL

## Cite

×

Formula_Derivatives-AFP

    @article{Formula_Derivatives-AFP,
      author  = {Dmitriy Traytel},
      title   = {Derivatives of Logical Formulas},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/Formula_Derivatives.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 28, 2015 : Isabelle2015