Verified decision procedures for MSO on words based on derivatives of regular expressions.
Dmitriy TraytelTobias NipkowPublished in: J. Funct. Program. (2015)
Keyphrases
- regular expressions
- decision procedures
- modal logic
- pattern matching
- theorem proving
- conjunctive queries
- finite automata
- query language
- automated reasoning
- tree automata
- semistructured data
- query evaluation
- query containment
- xml schema
- matching algorithm
- satisfiability problem
- theorem prover
- finite state machines
- context free grammars
- databases
- keywords
- inference rules
- temporal logic
- query answering
- relational databases