Tillämpad Logik DV1 (Applied Logic)

News

General information

• Course information, literature etc. ( PDF-fil )
• Language: the lectures, exercises and exam are given in English.
• This page will be updated regularly.
• Links to previous versions of the course can be found here: ht 2000, ht 2001, ht 2002.

Lectures

• schedule
• lecture plan (more details will appear later).
• Supplementary material
  • Oavgörbara problem i elementär aritmetik (page 7-8)
  • Equational logic.
  • Semantics of intuitionistic propositional logic (handed out).
  • Some logical background to the resolution method (handed out).
  • Demos of the theorem prover Otter.
  • Otter - an automatic theorem prover for first order logic

Exercises, hand-in problems and laboratory work

• Exercises and hand-in problems 1.
• Exercises and hand-in problems 2.
• Exercises and hand-in problems 3.
• Obligatory laboratory exercises (directory).
• Exercises and hand-in problems 4.

Examination

• Syllabus and typical exam questions. Literature allowed during exam.

Lecturers

• Erik Palmgren, main lecturer, professor.
• Fredrik Dahlgren, teaching assistant, PhD student in mathematical logic.

Links

• Mathematical logic in Uppsala.
• Summer course in Realiable Systems 5p held at the IT-department (Parosh Abdullah).
• Haskell -- a pure functional language.
• EQP - Equational Prover.
• List of systems for automatic theorem provers
• Program logic at Chalmers in Göteborg.
• BDD Portal
• Term rewritingsystems and XML: XSLT.
• Mathematica and term rewriting : Transformation rules.
• Course notes by Jeremy Avigad.
• Hilbert speaks on the radio 1930 "Wir müssen wissen, Wir werden wissen".