Formele logica

Het vak Formele Logica wordt gegeven aan studenten uit het tweede bachelorjaar in de informatica. Het omvat propositielogica en predicaatlogica met hun respectievelijke systemen van natuurlijke deductie. Verder worden temporele logica's CTL (computational tree logic) en LTL (linear temporal logic) besproken met modelverificatie in deze logica's. Als laatste worden enkele algoritmen met binaire beslissingsdiagrammen aangeleerd. De studiefiche voor Formele Logica is hier te vinden (English version).

De oefeningen voor Formele Logica omvatten enkele grote delen:

• Het trainen voor opstellen van formele bewijzen in predicaat- en propositielogica via online bewijsassistent ProofWeb.


• Enkele algoritmes op formules in de predicaatlogica leren, zoals het opstellen van de conjunctieve normaalvorm, het toepassen van een lineaire SAT-solver, en het werken met de algebraïsche normaalvorm van formules.


• Werken met de Java-applicatie Alloy, ontworpen om systemen te modelleren, en binnen zo'n systeem gerichte logische vragen te stellen. Alloy gaat dan na of er een model kan bestaan voor het systeem dat al dan niet aan je vragen voldoet.


• Leren werken in temporele logica's en het leren toepassen van het modelchecking algoritme voor CTL.


• Het opstellen van geordende en gereduceerde binaire beslissingsdiagrammen, alsook het toepassen van enkele algoritmes die hierop toe te passen zijn.

Het is de bedoeling om via een project één of meer van de aspecten van het vak wat dieper uit te werken en toe te passen. In 2013 was de opdracht een (eenvoudige) lift te modelleren in Alloy, en na te gaan of deze lift al dan niet voldeed aan wat men wilt van een lift. Bijvoorbeeld: als een persoon op de lift wacht, wordt deze persoon dan altijd opgehaald. Deze projectopgave kan je hier nalezen.