@INPROCEEDINGS{Basin93b,
AUTHOR = "David Basin and Sean Matthews",
TITLE = "A Conservative Extension of First Order Logic and its Applications to Theorem Proving",
BOOKTITLE = "13th Conference of the Foundations of Software Technology and Theoretical Computer Science",
Month = "December",
YEAR = 1993,
PAGES = "151--160",
NOTE          = {The paper available is an extended version of the Conference Paper},
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.},
}