Automatisches Beweisen über diskreten Strukturen

Kurzfassung: Viele komplexe  Aufgaben, die es heute und zukünftig in der Industrie zu bewältigen gilt, haben einen diskreten Anteil, welcher die Ursache für die besondere Schwierigkeit der zu lösenden Aufgaben darstellt. Solche Aufgaben lassen sich als mathematisches Beweisproblem formulieren, die von spezieller Software, sogenannte automatische Beweiser, voll automatisch gelöst werden können. Zu diesen Problemen gehören die Analyse und Optimierung von komplexen Produktdaten aber auch die präzise Beantwortung komplexer Anfragen auf einer Wissensbasis (Wiki). Die zu lösenden Probleme sind mindestens NP-hart. Dieser Vortrag zeigt sowohl Beispiele für Probleme, die sich mit automatischen Beweisern lösen lassen als auch Methoden die es ermöglichen die Lösungen trotz der hohen Komplexität meist in Echtzeit zu berechnen.