Introduction
Formele methoden is de benaming van een heel scala van technieken die zijn afgeleid van de mathematische logica en als doel hebben om een precieze (formeel vastgelegde) beschrijving en analyse van een computersysteem mogelijk te maken. De oudste formele methode is de (propositie of predicaten) logica zelf, waarin we eigenschappen van hardware, software of algoritmen kunnen opschrijven en nieuwe eigenschappen kunnen afleiden. Een formele methode wordt gekenmerkt door een formele taal (syntax) en een precies beschreven betekenis (semantiek) in de wereld om ons heen. Vaak worden formele methoden ondersteund door een computer programma ("tool") zodat we op een handige manier, gebruik makend van de rekenkracht van de computer, met deze formele methoden kunnen werken: automatisch eigenschappen afleiden, simulaties doen etc.. Er veel theorie over formele methoden zelf, om aan te tonen dat bepaalde mooie eigenschappen gelden. Bijvoorbeeld voor de predicatenlogica kun je bewijzen dat alles wat je kunt afleiden "waar" is en dat je niet alles kunt afleiden ("predicatenlogica is consistent").
In dit vak behandelen we de syntax en semantiek van propositie- en predicatenlogica, en als een bijzonder geval de taal voor logisch programmeren. Als tool zullen we werken met Otter, een stellingbewijzer ("theorem prover") die helpt bij het automatisch bewijzen van stellingen in de predicatenlogica. We zullen ook laten zien dat niet alles wat afleidbaar is automatisch bewezen kan worden door een computer (onbeslisbaarheid) en dat niet alles wat waar is afleidbaar is (onvolledigheid).
|
Objectives
- Natural deductions for proposition and predicate logic. Distinguish constructive and (essentially) non-constructive proofs
- Relation between syntax (language) and semantics (model) for proposition and predicate logic. Enkele veelgebruikte modeltheoretische eigenschappen onderzoeken en hun onderlinge verbanden verklaren.
- Operationele Semantiek van logisch programmeren vastleggen via resolutielogica.
- Operationele Semantiek van logisch programmeren vastleggen via Herbrandmodellen
- Mogelijkheden en beperkingen van predicaatlogische systemen aangeven met betekking tot uitdrukkingskracht en beslisbaarheid.
|
Subjects
Modellen van propositie- en predicatenlogica - Waarheidstabellen
- Waarheidsdefinitie van Tarski
- Volledigheidsstelling
Semantics of logic programming languages
- The resolution method for propositional and predicate logic
- Herbrand models and completeness of resolution
Axiomatic systems - Incompleteness of predicate logic (Gödel)
- Decidability of predicate logic
|
Study investment
- 16 hrs lecture
- 16 hrs question session
- 52 hrs individual study period
|
Teaching methods
lectures and research class ("responsie college")
|
Examination
deeltoetsen en een practicumopdracht
|
Pre-requisites
Beweren en Bewijzen
Semantiek en Correctheid
|
Literature
van Bentem et al - Logica voor Informatica.
Reeves and Clarke - Logic for computer science
|
