CS 498mp3: Logic in Computer Science: Skills list for final exam

All topics of midterm:

In general, you should know the material covered on the topics of propositional logic and first order logic, the theorems there, and consequences of them. While you do *not* have to be able to reproduce the proofs of major theorems, you should have understood them in reasonable detail so as to apply the techniques in other smaller problems. You are also encouraged to look at the homework problems and solutions. Some questions will be similar to these (but less hard as it is an exam setting). Some other specific skills you should know include:

• Propositional logic
  • Ability to model properties in propositional logic
  • Ability to apply the theorems in solving problems (e.g., using Konig's lemma or compactness theorem).
  • Ability to prove validity of formulas using resolution, formally.
  • Technical ability to be able to convert formulas to certain normal forms, in particular being able to put formula in CNF/
  • Ability to reduce satisfiability of propositional formulas to satisfiability in certain normal forma, especially CNF, and especially using polynomial blow-up (Tseitin's method).
• First-order logic
  • Ability to model properties in first-order logic.
  • Ability to construct models that satisfy/falsify given FO formulas
  • Ability to construct models and to work with them.
  • Ability to prove inexpressiveness of FOL using simply model constructions or using compactness theorem.
  • Know the *consequences* of the fundamental theorems (Godel's strong completeness theorem, incompleteness theorem, Compactness theorem, Lowenheim-Skolem theorem, and undecidability of FOL, in particular for FO theories).

  In addition, the following topics are included:

  Topics on first order theories, decidable theories of linear rationals using quantifier elimination, decidability of quantifier-free theory of equality, quantifier elimination and decidability of Presburger arithmetic, Nelson-Oppen combinations, automatic structures and FOL on automatic structures being decidable, monadic second-order logic on finite words and relationship with automata (as well as MSO on infinite words, trees, and infinite trees), interpretation (FO and MSO), etc.

  While you need to know the results in the above topics, you will need to know how to exhibit skills in the following:

  • The mechanism of quantifier elimination. Why quantifier elimination done recursively gives a ground formula and hence, typically, decidability.
  • Be able to do quantifier elimination for rationals using the standard algorithm we covered in class (and that's covered in detail in the book Calculus of Computation).
  • Definition of automatic structures. Being able to show a structure is automatic and hence show that it has a decidable FO theory.
  • Interpretations for first-order logic. Interpreting FOL on one structure in another, both the 1-tuple and k-tuple interpetations. Must be able to exhibit interpretations (like rationals to naturals, integers to naturals, and other fairly straightforward interpretations).
  • MSO on finite words. Must be able to exhibit an automaton for an MSO formula (which reads words with interpretations and accepts/rejects), and vice versa.
  -----------------------------------------------------------