| Veranstaltung: | 8745/8746 (Vorlesung mit Übungen) |
| Vorbesprechung: | keine |
| Termin: | Dienstag, 10 Uhr, Freitags 11, Übungen Dienstag 16 Uhr, jeweils ct |
| Beginn: | 1. Woche (also am 17. Oktober) |
| Ort: | Inf II, Raum 324 |
| Dozent: | Willem-Paul deRoever, Karsten Stahl und Martin Steffen |
| Univis: | Zentrale Daten |
Abstract: Unter Theorembeweisen versteht man das maschinenunterstützte Finden logischer Beweise. Es verbindet die Gebiete der mathematischen Logik mit algorithmischen Fragen nach effizienten Suchstrategien, adäquater Maschinenrepräsentierung und Organisation von Beweisen und anderem mehr. Mit Anwendungen von Logikprogrammierung über die Programmverifikation und Hardwaresynthese bis hin zu Datenbanken, Expertensystemen und künstlicher Intelligenz stellt Theorembeweisen eine wichtige Disziplin der Informatik dar. Ziel der Vorlesung ist es, in die Prinzipien des automatischen Beweisen und ihre algorithmischen Umsetzungen einzuführen sowie einen Einblick in den aktuellen Stand moderner Werkzeuge auf dem Gebiet zu geben.October 17, 2000
Von den Grundlagen der Aussagen- und Prädikatenlogik ausgehend wird die Vorlesung die wichtigsten für die Automatisierung geeigneten Beweissysteme behandeln, unter anderem Gentzensysteme und Systeme natürlichen Schließens sowie Resolutionsmethoden. Spätere Teile der Vorlesung behandeln die Umsetzung in verschiedene Klassen von Theorembeweisern. Ein Schwerpunkt der begleitenden Übungen wird der Umgang mit verschiedenen Beweiswerkzeugen sein.
This document was translated from LATEX by HEVEA and HACHA.