Beweise am Computer (PVS) * Logik und Beweissysteme ** Propositionale Logik ** Prädikatenlogik ** Logik höherer Stufe * Sequenzenkalküle * Automatische Verfahren * Typentheorie: Modularisierung (Beweisobjekte=Zertifikate, Berechnung von Beweisen) Praktischer Teil * Logikpuzzle * Verifikation von Algorithmen auf Listen und Bäumen * Hardwarekomponenten * Verteilte Algorithmen * Experimente mit anderen Systemen (Spass, Otter, Coq) VL Mi 12-14 Do 14-16 Ü Do 10.00 ct Z 11