Tillämpad Logik DV1

Uppläggningen av årets kurs kommer till stora delar vara identisk med fjolårets kurs: Tillämpad logik DV1, ht-2000

Aktuellt

Tillåtna hjälpmedel på tentamen förutom skrivdon:

I. Sigstam: Fullständighetssatsen för predikatlogiken via sekventkalkylen
W. Klop: Term rewriting systems

Schemaändring: Räkneövning 12/10 flyttas till 15/10, 15-17 sal 1113 pga konferens. Problemlösningssession 2 äger rum 15/10, 13-15 i sal 1145.

Gästföreläsare den 11 oktober: Lars-Henrik Eriksson, inst. för IT, avd. Datalogi och Industrilogik AB.

Sigstams kompendium Fullständighetssatsen för predikatlogiken via sekventkalkylen kan köpas för 20 SEK på UTH-gård, se karta. Alternativt kan Kleenes Mathematical Logic användas.

Allmänt

Kursinformation ( ps-fil | PDF-fil )
Schema och preliminär föreläsningsplan.
Läsanvisning ( ps-fil | PDF-fil )

Föreläsningar

Oavgörbara problem i elementär aritmetik ( ps-fil | PDF-fil )
Konstruktiv logik, kap 1-9 ( ps-fil | PDF-fil ).
Kompletterande material till termomskrivningssystem ( ps-fil | PDF-fil ).

Lektioner

Övningsblad 1 ( ps-fil | PDF-fil ). Facit ( ps-fil | PDF-fil ).
Övningsblad 2 ( ps-fil | PDF-fil ). Facit ( ps-fil | PDF-fil ).
Övningsblad 3 ( ps-fil | PDF-fil ). Facit ( ps-fil | PDF-fil ).
Övningsblad 4 ( ps-fil | PDF-fil ). Facit ( ps-fil | PDF-fil ).
Övningsblad 5 ( ps-fil | PDF-fil )
Övningsblad 6 ( ps-fil | PDF-fil )
Övningsblad 7 ( ps-fil | PDF-fil )

Laborationer

De båda laborationsuppgifterna är obligatoriska. För att ni skall få möjlighet att komplettera eller rätta ev. felaktigheter måste redovisningarna vara inlämnade 10 oktober. Sista inlämningsdag är annars 17 oktober.

Användarmanual för bevisredigeraren Alfa.
Anvisningar för laboration 1 ( ps-fil | PDF-fil )
Alfa-filer för laboration 1 finns här.
Anvisningar för laboration 2 ( ps-fil | PDF-fil )
Alfa-filer för laboration 2 finns här.
Några tips för användningen av den installerade versionen av Alfa
Exempel i Alfa:
- Pi och Sigma typer: uncurry
- Funktion definierade med ömsesidig rekursion (mutual recursion): mod 2.
- Övning 2.7 och 2.8.
- Gödel-Gentzens negativa översättning (mer avancerat)
- Avancerade exempel från Chalmers.

Examination

Kursen avslutas med en skriftlig tentamen den 17 oktober. Maximal skrivningspoäng är 40. För godkänt betyg krävs 18 poäng, för väl godkänt krävs 28 poäng. Upp till 3 bonuspoäng kan inräknas i skrivningsresultatet. Dessa kan erhållas genom att göra extra laborationsupggifter (se laboration 2) och/eller att lösa problem vid räkneövningstillfällena 27 september och 15 oktober.

Problem 1 den 27 september ( ps-fil | PDF-fil ).
Problem 2 den 15 oktober ( ps-fil | PDF-fil ).

Lärare

Erik Palmgren, föreläsningar, lektioner och laborationer.

Länkar

Programlogikgruppen vid Chalmers i Göteborg.
Otter - en automatisk teorembevisare för första ordningens logik
Lista av system för automatisk bevisföring
Termomskrivningssystem och XML: XSLT.
Mathematica och termomskrivningssystem : Transformationsregler.

6 juni 2002, Erik Palmgren.