Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Deriving Modular Programs from Short Proofs
| Book Series | Lecture Notes in Computer Science |
| Publisher | Springer Berlin / Heidelberg |
| ISSN | 0302-9743 (Print) 1611-3349 (Online) |
| Volume | Volume 2083/2001 |
| Book | Automated Reasoning |
| DOI | 10.1007/3-540-45744-5 |
| Copyright | 2001 |
| ISBN | 978-3-540-42254-9 |
| DOI | 10.1007/3-540-45744-5_47 |
| Pages | 561-577 |
| Subject Collection | Computer Science |
| SpringerLink Date | Monday, January 01, 2001 |
| |
|
Deriving Modular Programs from Short Proofs
Uwe Egly4  and Stephan Schmitt5
| (4) |
Institut für Informationssysteme 184/3, TU Wien, Favoritenstr. 9-11, A-1040 Wien, Austria |
| (5) |
Department of Sciences and Engineering, Saint Louis University, Madrid Campus, Avd. del Valle 34, 28003 Madrid, Spain |
Abstract
We present a polynomial translation of dag sequent proofs into tree sequent proofs for first-order classical and intuitionistic
logic. The basic idea is to interpret a reference in a dag proof as a lemma application, which is then simulated using an
application of the cut rule. The result of this translation is a tree proof with cuts, which are only applied in order to
“factorize” identical subproofs. We illustrate a central application of the presented cut-based translation, that is automated
extraction of modular programs from first-order intuitionistic proofs.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|