Kurzfassung

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 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.
» weiterlesen» einklappen