CS-316/CS-M16, Logic and Semantics

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)

News

(None. The course has finished for 2008/09, the exam has been written and is marked.)

Course Notes

Cumulated course notes (pdf) and slides (pdf) are available for all lectures so far. They will be updated together with the lecture log below.

Log

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

Assessment

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

Syllabus

The following gives an overview over the main topics covered by this module.

Propositional Logic
syntax, semantics, expressive completeness, normal forms, succinctness
First-Order and Second-Order Logic of Strings
syntax, semantics, linear temporal logic, Ehrenfeucht-Fraisse games, expressiveness, finite automata

Old News

Dec 2, 2008. Written exam will be on January 12, 2008.
Dec 2, 2008. Those of you haven't done it yet, please return the feedback forms. Additional feedback forms and printouts of the course notes can be found in Office 206, Farraday Building.
You can also provide feedback by sending me an email.
Dec 2, 2008. The lecture on Thursday, December 4 will be a general Question and Answer session on first-order logic, EF-games, MSO logic, and related (i.e., those topics not covered with the first two homework sheets). The general revision lecture will be, as announced, on December 9, 2008.
Nov 27, 2008. Revision lecture will be on Tuesday, December 9, 2008 at 11, Farraday-H.
Nov 26, 2008. The notes/slides are now also available in pdf format.
Oct 23, 2008. Dates for the next coursework are fixed: it will be handed out on Tuesday, October 28 and will be due on November 11. Most probably, the level M extra coursework will be handed out on November 18. There will be no lecture on November 25 (Gregynog).
Oct 20, 2008. Cumulated notes/slides are available and will be updated whenever the log is updated.
Oct 14, 2008. From now on the Thursday lectures will be given in Keir Hardie Building, room 430.
Oct 3, 2008. Dates for the first coursework fixed. It will handed out on Tuesday, October 7, and will be due on October 21, 2008.
Sep 30, 2008. Log of the lectures started, slides of today's lecture are available.
Sep 16, 2008. (Preliminary) date and times available. This module is to be taught Tue 11 and Thu 12. The full timetable is available elsewhere.
First lecture will be on Tuesday, September 30, 2008 at 11am in Faraday Building, room H.

$Date: 2009-02-06 09:59:04 $