Logic and Automata - Introduction
Satisfiability of : is there an interpretation in which is true.
Validity of : is true in all interpretations (reduces to satisfiability of ).
Some techniques for establishing this for quantified formulas:
- quantifier elimination (seen before)
- automata-based techniques - this lecture and next one
- game-based techniques (perhaps next week)
Common for quantifier elimination and automata-based techniques: characterize the set of all models (interpretations in which is true).
More generally, for each formula with free variables, we compute the relation that the formula defines.
We come up with a 'nice' representation of relations
- in quantifier elimination these are particular quantifier-free formulas
- in automata-based methods that we will look at, we represent relations as regular languages
In Lecture15 we have seen that Presburger arithmetic is decidable using quantifier elimination.
Today we see an alternative decision method, based on Presburger arithmetic, and then generalize it to more expressive logics: monadic second-order logic over strings and trees.