Logica en informatica

Van oudsher is logica de studie van het correct redeneren. Al in de klassieke oudheid hield men zich bezig met het analyseren van de structuur van redeneringen. Ook nu nog kan logica een belangrijk hulpmiddel zijn wanneer we de correctheid van een redenering willen onderzoeken. Logica wordt dan ook toegepast in tal van wetenschappen zoals taalkunde, filosofie en wiskunde. Een belangrijk recent toepassingsgebied is de informatica.

De cursus bestaat uit twee blokken.
In het eerste blok wordt een formele taal, de propositielogica, geïntroduceerd waarmee de structuur van redeneringen zichtbaar gemaakt kan worden. Zo kan 'waar rook is, is vuur' vertaald worden in r->v. Een formele taal wordt pas zinvol als de betekenis (semantiek) van deze taal is vastgelegd. De propositielogica maakt hiervoor gebruik van waarheidstabellen. De semantiek stelt ons in staat om te definiëren wanneer een formule een geldig gevolg is van een andere formule. Met behulp van semantische tableaus kan op een tamelijk efficiënte manier de geldigheid van een gevolgtrekking gecontroleerd worden. Naast deze semantische aanpak leer je in dit blok ook om met behulp van een axiomatisch systeem afleidingen te maken. Om beweringen waarin objecten, eigenschappen van objecten en variabelen een rol spelen te analyseren, is een rijkere taal nodig: die van de predikaatlogica. Deze taal staat centraal in het tweede blok van de cursus. Ook van de predikaatlogica wordt zowel de semantiek als een axiomatisch bewijssysteem uitgelegd. De cursus behandelt twee toepassingen van de predikaatlogica binnen de informatica. De eerste toepassing is gericht op imperatieve talen. Je leert hoe 'Hoare-calculus' gebruikt kan worden om de correctheid van programma's te bewijzen. Bij het tweede onderwerp, logisch programmeren, maak je kennis met algemene resolutie en stellingbewijzen met behulp van skolemiseren.

Leerdoelen
Na bestudering van deze cursus kun je:
- semantische tableaus gebruiken om de geldigheid en constistentie te controleren, en om te onderzoeken of een formule een tautologie is,
- axiomatische bewijzen geven in zowel propositielogica als predikaatlogica,
- bewijzen over logica leveren met formule-inductie,
- resolutiebewijzen geven, en met behulp van herschrijven, Skolemvormen en unificatie ook algemene resolutie toepassen,
- bij een STIP-programma een begin-bedeling een eind-bedeling bepalen,
- met behulp van Hoarecalculus de correctheid van eenvoudige programma’s bewijzen,
- predikaatlogische formules interpreteren op modellen, en bij predikaatlogische formules modellen en tegenmodellen zoeken.

Na het bestuderen van de cursus heb je inzicht in de mogelijkheden en beperkingen van de logische taal en inzicht in het onderscheid tussen syntax en semantiek.