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 einzelnen Teilbereiche in der...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