MPI-I-93-235. August 1993, 11 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry
Abstract in LaTeX format:
We define a weak second--order extension of first--order logic.
We prove a second--order cut elimination theorem for this logic
and use this to prove a conservativity and a realisability
result. We give applications to formal program development and
theorem proving, in particular, in modeling techniques
in formal metatheory.
References to related material:
|To download this research report, please select the type of document that fits best your needs.||Attachement Size(s):|
|MPI-I-93-235.pdf - MPI-I-93-235.dvi||43 KBytes; 77 KBytes|
|Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView|