Ansprechpartner:	Serge AUTEXIER, Geb. 36, Zi. 210	30. Januar 1998
	Dieter HUTTER, Geb. 36, Zi. 214

Im Rahmen der formalen Software-Entwicklung werden Beweissysteme zur Verifikation von anfallenden Beweisverpflichtungen eingesetzt. Diese Beweiser sollten zum einen einen hohen Automatisierungsgrad haben, müssen aber auch ad"aquate Möglichkeiten zur Benutzerinteraktion anbieten. Da die zu führenden Beweise oft sehr lang sind, ist es nicht sinnvoll, dem Benutzer nur die Möglichkeit zu geben auf Kalkülebene in die Beweiskonstruktion eingreifen zu können; vielmehr sollte der Benutzer in der Lage sein, auf einer hierarchisch hoch angesiedelten Ebene lenkend in die Beweissuche einzugreifen. Dies wird zum Beispiel durch ein planbasiertes hierarchisches Vorgehen ermöglicht, was aber zur Folge hat, daß die automatischen Beweiskomponenten auch planbasiert vorgehen müssen.

Die HIWI Tätigkeit besteht darin, einzelne Programmieraufgaben zu übernehmen, die bei der Entwicklung einer Beweisplanungskomponente für bestehende Beweiser anfallen.

Voraussetzungen: Kenntnisse in Logik und der Programmiersprache LISP.