<div class="csl-bib-body">
<div class="csl-entry">Rukhaia, M. (2009). <i>CERES and fast cut-elimination</i> [Master Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/186564</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/186564
-
dc.description
Zsfassung in dt. Sprache
-
dc.description.abstract
Es ist bekannt dass die Komplexitat der Schnittelimination im allgemeinen Fall nonelementar ist. In dieser Arbeit werden Klassen von Beweisen charakterisiert welche eine schnelle (elementare) Schnittelimination zulassen. Zuerst werden der Sequentialkalkul und der Resolutionskalkul eingefuhrt. Anschliessend werden zwei Methoden der Schnittelimination, die Methode von Gentzen und CERES (cut-elimination by resolution), beschrieben. Es wird gezeigt, dass CERES die Gentzen Methode nonelementar beschleunigt. Die Methode CERES wird dann verwendet um schnelle Schnitteliminationsklassen zu definieren. Einige der bekannten Klassen werden erweitert und nachgewiesen, dass die Schnittelimination schnell bleibt. Schliesslich wird eine neue Klasse ONEQ eingefuhrt und (ebenfalls mit der CERES-Methode) nachgewiesen, dass schnelle Schnittelimination auf ONEQ moglich ist.
