TDDC53 Logic II 2007

Study Guide@lith

Valid for year : 2007

TDDC53	Logic II, 4,5 ECTS credits. /Logic II/ For: CS
OBS!	Only open for students admitted to the Computer Science Master programme
	Prel. scheduled hours: Rec. self-study hours: 120
	Area of Education: Technology Subject area: Computer Science
	Advancement level (G1, G2, A): A
	Aim: The course goal is to provide the participants with a broad knowledge on modern logics and their applications in computer science, in particular in artificial intelligence, automated theorem proving and formal specification and verification of software. Issues on incomplete and inaccurate information are also discussed. The participans will learn how to chose and/or develop a logic for a particular application domain together with proof systems, with the emphasis on automated verification of satisfiability and validity of formulas.
	Prerequisites: (valid for students admitted to programmes within which the course is offered) Introductory course in logic. Note: Admission requirements for non-programme students usually also include admission requirements for the programme and threshhold requirements for progression within the programme, or corresponding.
	Organisation: The course is given in an intensive format ("crash course").
	Course contents: Proof and model theory: soundness and completeness, semantic tableaux, natural deduction, sequent calculus, resolution, Horn theories, logic programming. Not all proof methods will be covered, but selected methods will be covered in depth. Selected issues in meta theory of which the following are representative issues: Lowenheim-Skolem theorem, Herbrand's theorem, compactness, Lindström's theorem, Gödel's incompleteness theorem, axiomatization of natural, rational and real numbers. Introduction to non-standard logics: modal logic, 2nd-order logic.
	Course literature: Lecture notes.
	Examination:
	Take home exam.	3 p	/	4,5 ECTS

	Grades given are Pass, Fail.
Course language is English. Department offering the course: IDA. Director of Studies: Examiner: Andrzej Szalas Course Syllabus in Swedish

Linköping Institute of Technology
Contact: TFK , val@tfk.liu.se Last updated: 04/04/2007