Beweisplanen mit Hilfe von Differenz-Reduktionstechniken

点击翻译按钮获取中文摘要

Ziel des Fortsetzungsprojektes DiReCT2 ist es nun zu untersuchen, wie diese von uns im ersten Projektabschnitt entwickelten Verfahren sowie entsprechend erweiterte Knuth-Bendix Vervollständigungsverfahren in ein übergeordnetes Planbasiertes Beweisverfahren integriert werden können. Planbasiertes Beweisen ist ein von der Forschungsgruppe in Saarbrücken entscheidend mitgeprägtes neues Paradigma der Deduktion, in dem Beweise zunächst auf einer sehr abstrakten Ebene geplant und dann sukzessive zu einem Objektbeweis verfeinert werden. Diese neuen Verfahren gestatten es, Beweise von einer Länge zu synthetisieren, die um ein bis zwei Größenordnungen über denen traditioneller Suchverfahren liegen. Wir wollen nun als erstes untersuchen, wie man Knuth-Bendix basierte Vervollständigungsverfahren so erweitern kann, daß sie auf den von uns entwickelten annotierten Termen arbeiten. Knuth-Bendix Verfahren haben sich in der Vergangenheit zur Behandlung von Gleichheitsproblemen durchgesetzt; der mit Abstand schnellste Beweiser für Gleichheitsprobleme, das Waldmeister-System, basiert auf dem Knuth-Bendix Verfahren. Darüber hinaus können Vervollständigungsverfahren zur Erzeugung neuer Lemmata verwendet werden, um damit Planbasierte Verfahren zu unterstützen, die auf solche zusätzlichen Informationen angewiesen sind. Vervollständigungsverfahren dienen auch zur Erzeugung von Entscheidungsverfahren oder Simplifikationsroutinen bezüglich ausgewählter Gleichungsmengen. Analog zu anderen Entscheidungsverfahren stellt sich dabei die Frage, wie solche Verfahren in erweiterten Theorien, d. h. bei Anwesenheit zusätzlicher Axiome als Semi-Entscheid- ungsverfahren eingesetzt werden können. In einem zweiten und abschließenden Schritt sollen die bereits entwickelten differenz-reduzierenden Verfahren des ersten Förderabschnittesund die erweiterten Knuth-Bendix Verfahren in ein überge- ordnetes Planbasiertes Vorgehen integriert werden. Mit dieser zweiten Förderphase soll das Projekt abgeschlossen werden, um danach die Ergebnisse in ein kommerzielles System zur Verifi- kation im DFKI im Rahmen einer Transferförderung zu inte- grieren.