Bitte warten...
Bitte warten...
English
Hilfe
Login
Forschungsportal
Suche
Forschungsprofile
Forschungsprojekte
Projektvollmacht
Lehre
Forschung
Organisation
Semantische Charakterisierung der Schnittelimination
01.03.2006 - 30.11.2009
Forschungsförderungsprojekt
Schnittelimination ist eine der wichtigsten Techniken der Beweistheorie. Grob gesprochen erzeugt die Schnittelimination aus einem Beweis einen Beweis ohne Lemmata, der im wesentlichen aus den syntaktischen Bestandteilen des bewiesenen Satzes aufgebaut ist. Seit ihrer Einführung im Jahr 1934 sind Sequenzenkalküle eine der bevorzugten Instrumente der Formalisierung des Schließens in Logiken. Dieses Instrument ist jedoch nicht geeignet alle nützlichen und interessanten Logiken zu untersuchen. Aus diesem Grund wurde in den letzten Dekaden eine große Anzahl von Varianten und Erweiterungen des Gentzenschen Sequenzenkalküls eingeführt. Unter diesen gelten Hypersequenzenkalküle als besonders elegante und einfache Grundlage für "logical engineering" mit Anwendung auf zahlreiche nichtklassische Logiken. Ziel des vorliegenden Projektes ist eine semantische Charakterisierung der Schnittelimination in Sequenzen- und Hypersequenzenkalkülen. Damit ist die Formulierung von syntaktischen und semantischen Kriterien gemeint, die -- falls erfüllt -- eine bevorzugte Variante der Schnittelimination für den gegebenen Kalkül garantieren, andernfalls die Konstruktion eines Gegenbeispiels zu dieser bevorzugten Schnittelimination erlauben. Dabei stehen folgende Fragen im Mittelpunkt: Was sind natürliche Eigenschaften für Regeln, die Schnittelimination erhalten? Gibt es eine uniforme Methode um für eine große Klasse von Sequenten- und Hypersequenkalkülen die Eliminierbarkeit der Schnitte zu beweisen oder zu widerlegen? Die entscheidenden Vorteile einer solchen Methode wären: 1. Erleichterung des Nachweises der Schnittelimination für neue Kalküle und der Erstellung von analytischen Kalkülen für neue Logiken. 2. Möglichkeit der automatischen Erzeugung von Schnitteliminationsmethoden und der automatischen Überprüfung der zugehörigen formalen Kriterien.
Personen
Projektleiter_in
Univ.Prof.in Dr.in Agata Ciabattoni
(E104)
Projektmitarbeiter_innen
Vesna Sabljakovic-Fritz
(E104)
Dr.techn. Clemens Richter
(E104)
Projektass.in(FWF) Nino Antidze MD
(E104)
George Metcalfe
(E104)
Mag.rer.nat. Dr.techn. Oliver Fasching
(E104)
Eva Rusnokova
(E104)
Institut
E104 - Institut für Diskrete Mathematik und Geometrie
Förderungsmittel
FWF - Österr. Wissenschaftsfonds (National)
Fonds zur Förderung der wissenschaftlichen Forschung (FWF)
Forschungsschwerpunkte
Information and Communication Technology
Schlagwörter
Deutsch
Englisch
hypersequent calculi
hypersequent calculi
cut elimination
cut elimination
proof theory
proof theory
non classical logics
non classical logics