Logic

VU 3   WS 2006/07   LVA 703600

Description

The lecture is an introduction to formal logic and the theory of automated deduction.

There are no prerequisites, but the learning curve is less steep if you have already heard Logic in Computer Science (Algorithmische Mathematik 7).

Content

• Inductive vs. deductive reasoning
  
• Propositional Logic: syntax & semantics
• Propositional Logic: proof systems
• First-Order Logic: syntax & semantics
• First-Order Logic: proof systems
• Resolution
  

Literature

The lecture is based on

Mordechai Ben-Ari: Mathematical logic for computer science.
Springer, 2nd ed. 2004. ISBN: 1-85233-319-7.

with occasional additional material. A small number of copies will be available in the Semesterapparat. A similar exposition of the material is

Melvin Fitting, First-Order Logic and Automated Theorem Proving.
Springer, 2nd ed., 1996. ISBN: 0-387-94593-8.

Fitting's treatment of the subject is more formal. The book is out of print, but a few copies are available in the library. Finally, a German book on the subject is

Uwe Schöning, Logik für Informatiker.
Spektrum Akademischer Verlag, 5. Aufl., 2000. ISBN 3827410053.

This is a good supplementary book for the course if you prefer something in German. It does not cover all the proof systems we will present, though.