Logic

A course by Lutz Schröder at the Universität Bremen 2004.

Formal logic is the foundation of mathematics, and hence of computer science as well. Indeed, logic plays an even more central role in computer science than in `traditional' mathematics, since computer science places much more emphasis on exactness of the syntax and semantics of statements. In particular, the latter are a prerequisite for the mechanized treatment of statements, e.g. in algebraic specification languages or automatic provers, but also in many formalisms of modern AI.

This course provides an introduction into so-called first order logic, using the textbook `Language, Proof and Logic' by Jon Barwise and John Etchemendy, the purchase of which is strongly recommended to course participants. Proofs using the proof system Fitch (the software comes with the book) will be set as exercises.

NEW: Assessment Criteria (in German) NEW DEADLINES!!

NEW: The problem sheet is due on July 13, 2004 (NEW DEADLINE!)

Hinweise zum Ausfüllen des Scheinformulars; Abgeben nicht vergessen!

NOTE: Timeouts from the Grade Grinder usually mean that your formalization is incorrect!!

NEW: Results of assessment (in German)

Teaching Material

• Slides on Languages and Models
• Slides on Satisfaction
• The LPL software can be found under /usr/local/pub-bkb/lpl (local access only)
• Slides on Logical Consequence
• Slides on Equational Rules
• Slides on Normal Forms
• Slides on Truth Tables
• Slides on Soundness
• Slides on Quantifiers
• Slides on Proof Rules for Quantifiers
• Slides on NNF for FO Formulae
• Slides on prenex NF and Resolution
• Slides on Skolemization and Unification
• Slides on Completeness of Propositional Logic

Examples

• Proof of set exercise, version 1
• Proof of set exercise, version 2
• A proof by contradiction
• Currying implications
• Uncurrying implications
• An equivalence proof
• Symmetry of equivalence
• Concatenating two implications
• Exploiting non-emptyness of the domain
• Interchanging universal quantification and conjunction
• De Morgan's Law for quantifiers
• Proof of second set exercise