Transformation in Normalform, Semantische Baeume, Unifikation, Resolution, Verfeinerungen der Resolution, Paramodulation, Experimente mit Automatischen Beweisern. Didaktisches Vorgehen: waehrend der Lehrveranstaltung werden 2 Gruppen von Aufgaben verteilt welche mit Hilfe des Beweisers prover9 zu loesen sind. Muendliche Abschlusspruefung.
Aufwandsabschaetzung
54h: 18 Vorlesungseinheiten a 2std + 1Std Vorbeitung
8h: Loesen erstes Uebungsblatt
2h: tippen der Loesungen in LaTeX
8h: downloaden und Testen von prover9
34h: Loesen 2. Uebungsblatt (mit Hilfe von prover9)
3h: tippen der Loesungen in LaTeX
40h: Vorbereitung auf abschl. Pruefung
1h: abschliessende Pruefung
-----------------------------------------------------------
150 h = 6 ECTS