This is an old revision of the document!
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).
Example: \[
\exists x. \exists y.\ z = 3 x + 1 \land z = 5 y + 3
\]
In Lecture15 we have seen that Presburger arithmetic is decidable using quantifier elimination.
Today we look at a different decision method for Presburger arithmetic, which generalizes to certain more expressive logics (monadic second-order logic over strings and trees).