Test-sets und Termersetzungen für die Generierung rekursiv definierter Algorithmen aus Existenzaussagen

Abstract

In dieser Arbeit wurde ein Verfahren vorgestellt, mit dem man rekursiv definierte Algorithmen aus Gueltigkeitsbeweisen von Existenzformeln extrahieren kann.Das Verfahren beschränkt sich auf einen einfachen Formalismus und basiert auf Test-sets und einem Vereinfachungsmechanismus.Termersetzungen und logische Simplifikationen bilden den Kern dieses Vereinfachungsmechanismus, waehrend Test-sets eine Beschreibung des initialen Modells einer Axiommenge darstellen.

In this thesis we presented a method for extracting recursive defined algorithms from existentially quantified formulas, being based on a simple formalism, test sets and a simplification strategy.Term rewriting and logical simplification represent the core of that simplification strategy and test sets the description of the initial model of a set of axioms.