de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Report

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

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44075

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

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45002

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

Locator
There are no locators available
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: http://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.