Erzeugung von Inferenzsytemen für nicht-klassische Logiken

Es gibt leider keine einzelne Logik, die fuer alle Anwendungen angemessen ist. Dazu kommt noch, dass bei ueblichen Anwendungen die geeignetste Logik im Allgemeinen nicht im vorhinein bestimmbar ist. Es ist deshalb notwendig, grosse Familien von Logiken zu untersuchen und moeglichst uniforme Kalkuele zu entwickeln, die es erlauben, muehelos von einer Logik auf die andere ueberzugehen und die Beziehung zwischen den Logiken besser zu verstehen. Es ist deshalb eine Hauptaufgabe der Logik in der Informatik, die automatische Erzeugung von analytischen Kalkuelen fuer einen breiten Bereich von nichtklassischen Logiken zu gewaehrleisten. (Analytische Kalkuele sind Kalkuele, die eine Beweissuche durch eine schrittweise Zerlegung der zu beweisenden Formel ermoeglichen.) Das beruehmteste Beispiel eines analytischen Kalkueles ist der Kalkuel LK von Gentzen. Gentzen-artige Kalkuele dienen dem Automatischen Beweisen und erlauben die Gewinnung von wichtigen impliziten Informationen aus Beweisen, z.B.Schranken oder Programme im Beweisformat. Ausserdem sind sie ein Schluessel zum Verstaendnis der Syntax-Semantik Beziehung. Ziel dieses Projektes ist es, Verfahren zur automatischen Generierung von analytischen Sequent- und Hypersequentkalkuelen fuer grosse Klassen von Logiken zu entwickeln. Das vorliegende Projekt plant die Entwicklung von * Metatheorembeweisern, die bei gegebener Logik existierende Automatische Beweiser auf eben diese Logik adaptieren. *Modularen Schnitteliminationsmethoden, die auf Transferprinzipien aufbauen, und es erlauben, die Schnittelimination von Unterklassen von Kalkuelen auf die Gesamtheit der Kalkuele auszudehnen. *Verfahren, die Beweise automatisch analysieren, d.h. die eine automatische Entnahme von impliziten Informationen wie numerische Schranken und (Varianten von) Herbrand Disjunktionen ermoeglichen.