Number of cases campus Koblenz: 1 (warning level Gelb until 02.12.2020) Action plan

Entscheidungsverfahren für komplexe logische Theorien

Period: Jan 01, 2005 - Dec 31, 2025
Status: laufend

Die formale Beschreibung bestimmter Systeme ist aus Teilen zusammengesetzt, die verschiedenen Bereichen entstammen. So finden sich beispielweise in der Beschreibung eines Programms numerische Formeln neben Aussagen über Datenstrukturen; die Beschreibung ist entsprechend komplizierter 
für komplexe Systeme mit embedded Software mit Zugriff auf verschiedenen Datenbanken. 

Um solche Systeme zu modellieren, benutzen wir Kombinationen von logischen Theorien, die die einzelnen Teilbereiche in der Beschreibung des Systems formalisieren. 

 

Das Ziel dieses langjährigen Projektes ist es, Beweisverfahren für diese Art von komplexen logischen Theorien zu entwickeln, welche die modulare Struktur der Theorien ausnutzen und es erlauben, spezialisierte Beweiser für das Schlussfolgern in den Teiltheorien zu benutzen. Solche modularen Verfahren sind besonders flexibel und effizient und in vielen Bereichen anwendbar (wie etwa in der Mathematik, in der Verifikation oder in der Wissensrepräsentation). 


Unsere Methoden wurden im Theorembeweiser H-PILoT implementiert.