On the form of witness terms |
| |
| Authors: | Stefan Hetzl |
| |
| Institution: | 1. Laboratoire Preuves, Programmes et Systèmes (PPS), Université Paris Diderot, 175 Rue du Chevaleret, 75013, Paris, France
|
| |
| Abstract: | We investigate the development of terms during cut-elimination in first-order logic and Peano arithmetic for proofs of existential
formulas. The form of witness terms in cut-free proofs is characterized in terms of structured combinations of basic substitutions.
Based on this result, a regular tree grammar computing witness terms is given and a class of proofs is shown to have only
elementary cut-elimination. |
| |
| Keywords: | |
| 本文献已被 SpringerLink 等数据库收录！ |
|
