Information for the module "Logic and Semantics" as taught in the academic year 2008/09 (Computer Science, Swansea University).
Lecturer: | Klaus Aehlig |
Date/Time: | Tue 11 in Far-H and Thu 12 in KH-430 (first teaching block) |
2.12.08 |
Automata-theoretic proof of Büchi's Theorem, Presburger
Arithmetic.
Notes, slides |
27.11.08 |
revised Büchi's Theorem; started sketch of an
automata-theoretic proof (will be finished next lecture; not part
of the exam syllabus)
Notes, slides |
20.11.08 |
MSO games; MSO games on unstructured sets; Büchi's Theorem
(semantic proof); some consequences of Büchi's Theorem
Notes, slides |
18.11.08 |
MSO games, correspondence to formulae of bounded quantifier rank,
finiteness of the types of bounded quantifier rank.
Notes, slides. course work for level M students only. |
13.11.08 |
discussion solutions to coursework 2. Example of describing a run
of an NFA by an MSO formula.
Notes, slides |
11.11.08 | syntax and semantics of monadic second-order logic; MSO can
define all regular properties
Notes, slides |
6.11.08 |
EF-games on linear orders; hinted on syntax and semantics of
monadic second-order logic (will be done properly next lecture).
Notes, slides |
4.11.08 |
finished the proof the Ehrenfeucht-Faisse Theorem; EF-games on
unstructured sets; started EF-games on linear orders (will be done
in more detail in the next lecture)
Notes, slides |
30.10.08 |
Revised Ehrenfeucht-Faisse Games, introduced the notion of the
quantifier-rank, started the proof of the Ehrenfeucht-Faisse
Theorem (will be revised and finished next lecture).
Notes, slides |
28.10.08 |
Handed out second course work (due November 11). Negation and
Prenex normal forms for first-order logic; Ehrenfeucht-Faisse Games.
Notes, slides, course work |
23.10.08 |
embedding of LTL into first-order logic. Discussed solutions to coursework 1.
Notes, slides |
21.10.08 |
syntax and semantics of first-order logic.
Notes, slides |
16.10.08 |
Automata description of LTL, Consequences (satisfiability,
regularity, size of models); hinted on first-order logic (will be
done properly next lecture)
Notes, slides |
14.10.08 |
syntax and semantics of LTL; LTL model checking; LTL and finite
automata; hinted on Corollaries: satisfiability, regularity, size
of models (will be revised next lecture)
Notes, slides |
9.10.08 | first-order structures for finite traces and words; started
syntax and semantics of LTL (will be revised next lecture)
Notes, slides |
7.10.08 | Handed out first course work sheet.
Revised expressional completeness. Size of formulae
(non-succinctness); model-checking problem is in P; satisfiability
is NP-complete.
Notes, slides, course work |
2.10.08 | Revised syntax of propositional logic; defined its semantics;
free variables and coincidence-lemma as example for using
inductively defined data (like formulae); expressional
completeness and disjunctive normal forms; other complete bases.
Notes, slides |
30.09.08 | Administrative information, overview over the course; syntax
of propositional logic, hinted on its semantics (will be repeated
next lecture). Notes, slides |
CS-316: | 20% coursework (2 assignments during the term) 80% exam at end of term |
CS-M16: | 30% coursework (3 assignments during the term) 70% exam at end of term |
The following gives an overview over the main topics covered by this module.
$Date: 2009-02-06 09:59:04 $