Beweisanalyse und autom. Deduktion für rekursive Strukturen

In der Beweistheorie betrachtet man Beweise als Objekte. Die formale Beweisanalyse befasst sich mit rechnerischen Transformationen dieser Objekte, um die Beweise zu untersuchen. Beispielsweise könnte man an der Essenz eines Beweises interessiert sein, welche sich durch die Extraktion von Information aus dem Beweis gewinnen lässt. Diese Art von Informationsgewinnung aus einem formalen Beweis basiert auf dem sogenannten Satz von Herbrand. Durch die Gewinnung dieser Art von Information aus einem Beweis eines Satzes erhalten wir aussagekräftige Informationen über die in dem Satz vorkommenden Variablen oder deren oberen und unteren Schranken. Mathematische Induktion ist eines der wesentlichen Konzepte im Werkzeugkasten des Mathematikers, jedoch erschwert seine Verwendung die formale Beweisanalyse. Im Wesentlichen komprimiert die Induktion ein unendliches Argument zu einer endlichen Aussage. Dieser Prozess verschleiert aber Information, die für die rechnerische Beweistransformation und das automatisierte Schließen unerlässlich ist. Der Satz von Herbrand deckt die klassische Prädikatenlogik ab. Während es Interpretationen des Satzes von Herbrand gibt, die seinen Geltungsbereich auf Induktion ausdehnen, so gehen diese Ergebnisse auf Kosten der Analytik, die aber die wünschenswertesten Eigenschaft des Satzes von Herbrand ist, da sie für die Informationsgewinnung aus Beweisen verwendet wird. Angesichts der zunehmenden Bedeutung der formalen Mathematik und des induktiven Beweisens für viele Bereiche der Informatik ist die Entwicklung unseres Verständnisses der Analytizitätsgrenze von entscheidender Bedeutung. In diesem Projekt gehen wir diese Probleme an, indem wir eine relativ neue Formulierung der Induktion als Folge von Beweisen verwenden, die als Beweisschemata bezeichnet werden. Diese Art der zyklischen Darstellung hat in den letzten Jahren an Zugkraft gewonnen und wird aller Wahrscheinlichkeit nach in den kommenden Jahren eine wesentliche Rolle im automatisierten Beweisen und in der Beweistheorie spielen. Im Gegensatz zu anderen Ansätzen der zyklischen Beweistheorie konzentrieren wir uns jedoch auf die Extraktion einer endlichen Darstellung der in formalen Beweisen enthaltenen Information. Unser Hauptziel ist die Entwicklung einer rechnergestützten beweistheoretischen Methode zur Extraktion dieser Information für aussagekräftige induktive Theorien.

In der Beweistheorie betrachtet man Beweise als Objekte. Die formale Beweisanalyse befasst sich mit rechnerischen Transformationen dieser Objekte, um die Beweise zu untersuchen. Beispielsweise könnte man an der Essenz eines Beweises interessiert sein, welche sich durch die Extraktion von Information aus dem Beweis gewinnen lässt. Diese Art von Informationsgewinnung aus einem formalen Beweis basiert auf dem sogenannten Satz von Herbrand. Durch die Gewinnung dieser Art von Information aus einem Beweis eines Satzes erhalten wir aussagekräftige Informationen über die in dem Satz vorkommenden Variablen oder deren oberen und unteren Schranken. Mathematische Induktion ist eines der wesentlichen Konzepte im Werkzeugkasten des Mathematikers, jedoch erschwert seine Verwendung die formale Beweisanalyse. Im Wesentlichen komprimiert die Induktion ein unendliches Argument zu einer endlichen Aussage. Dieser Prozess verschleiert aber Information, die für die rechnerische Beweistransformation und das automatisierte Schließen unerlässlich ist. Der Satz von Herbrand deckt die klassische Prädikatenlogik ab. Während es Interpretationen des Satzes von Herbrand gibt, die seinen Geltungsbereich auf Induktion ausdehnen, so gehen diese Ergebnisse auf Kosten der Analytik, die aber die wünschenswertesten Eigenschaft des Satzes von Herbrand ist, da sie für die Informationsgewinnung aus Beweisen verwendet wird. Angesichts der zunehmenden Bedeutung der formalen Mathematik und des induktiven Beweisens für viele Bereiche der Informatik ist die Entwicklung unseres Verständnisses der Analytizitätsgrenze von entscheidender Bedeutung. In diesem Projekt gehen wir diese Probleme an, indem wir eine relativ neue Formulierung der Induktion als Folge von Beweisen verwenden, die als Beweisschemata bezeichnet werden. Diese Art der zyklischen Darstellung hat in den letzten Jahren an Zugkraft gewonnen und wird aller Wahrscheinlichkeit nach in den kommenden Jahren eine wesentliche Rolle im automatisierten Beweisen und in der Beweistheorie spielen. Im Gegensatz zu anderen Ansätzen der zyklischen Beweistheorie konzentrieren wir uns jedoch auf die Extraktion einer endlichen Darstellung der in formalen Beweisen enthaltenen Information. Unser Hauptziel ist die Entwicklung einer rechnergestützten beweistheoretischen Methode zur Extraktion dieser Information für aussagekräftige induktive Theorien.