Logic IIFDA144, 2004VT
|
|
Course plan
Lectures
Approximately 24 hours.
Recommended for
Doctoral students with some background in logics (e.g. introductory course).
The course was last given
Spring 2003
Goals
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
Introductory course in logic
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.
Organization
The course is given in an intensive format ("crash course").
Literature
Lecture notes
Lecturers
Andrzej Szalas
Examiner
Andrzej Szalas
Examination
Take home exam/assignment.
Credit
2.5 credits
Comments
Course web page
Click here for more information.
Page responsible: Anne Moe