English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

Released
Report

A conservative extension of first-order logic and its application to theorem proving

MPS-Authors
/persons/resource/persons44075

Basin,  David
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45002

Matthews,  Seán
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

MPI-I-93-235.pdf
(Any fulltext), 78KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Basin, D., & Matthews, S.(1993). A conservative extension of first-order logic and its application to theorem proving (MPI-I-93-235). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-B48B-0
Abstract
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.