doc-src/ZF/logics-ZF.bbl

-\begin{thebibliography}{10}
-
-\bibitem{abrial93}
-J.~R. Abrial and G.~Laffitte.
-\newblock Towards the mechanization of the proofs of some classical theorems of
-  set theory.
-\newblock preprint, February 1993.
-
-\bibitem{basin91}
-David Basin and Matt Kaufmann.
-\newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison.
-\newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical
-  Frameworks}, pages 89--119. Cambridge University Press, 1991.
-
-\bibitem{boyer86}
-Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and
-  Lawrence Wos.
-\newblock Set theory in first-order logic: Clauses for {G\"{o}del's} axioms.
-\newblock {\em J. Auto. Reas.}, 2(3):287--327, 1986.
-
-\bibitem{camilleri92}
-J.~Camilleri and T.~F. Melham.
-\newblock Reasoning with inductively defined relations in the {HOL} theorem
-  prover.
-\newblock Technical Report 265, Computer Laboratory, University of Cambridge,
-  August 1992.
-
-\bibitem{davey&priestley}
-B.~A. Davey and H.~A. Priestley.
-\newblock {\em Introduction to Lattices and Order}.
-\newblock Cambridge University Press, 1990.
-
-\bibitem{devlin79}
-Keith~J. Devlin.
-\newblock {\em Fundamentals of Contemporary Set Theory}.
-\newblock Springer, 1979.
-
-\bibitem{dummett}
-Michael Dummett.
-\newblock {\em Elements of Intuitionism}.
-\newblock Oxford University Press, 1977.
-
-\bibitem{dyckhoff}
-Roy Dyckhoff.
-\newblock Contraction-free sequent calculi for intuitionistic logic.
-\newblock {\em J. Symb. Logic}, 57(3):795--807, 1992.
-
-\bibitem{halmos60}
-Paul~R. Halmos.
-\newblock {\em Naive Set Theory}.
-\newblock Van Nostrand, 1960.
-
-\bibitem{kunen80}
-Kenneth Kunen.
-\newblock {\em Set Theory: An Introduction to Independence Proofs}.
-\newblock North-Holland, 1980.
-
-\bibitem{noel}
-Philippe No{\"e}l.
-\newblock Experimenting with {Isabelle} in {ZF} set theory.
-\newblock {\em J. Auto. Reas.}, 10(1):15--58, 1993.
-
-\bibitem{paulin-tlca}
-Christine Paulin-Mohring.
-\newblock Inductive definitions in the system {Coq}: Rules and properties.
-\newblock In M.~Bezem and J.F. Groote, editors, {\em Typed Lambda Calculi and
-  Applications}, LNCS 664, pages 328--345. Springer, 1993.
-
-\bibitem{paulson87}
-Lawrence~C. Paulson.
-\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
-\newblock Cambridge University Press, 1987.
-
-\bibitem{paulson-set-I}
-Lawrence~C. Paulson.
-\newblock Set theory for verification: {I}. {From} foundations to functions.
-\newblock {\em J. Auto. Reas.}, 11(3):353--389, 1993.
-
-\bibitem{paulson-CADE}
-Lawrence~C. Paulson.
-\newblock A fixedpoint approach to implementing (co)inductive definitions.
-\newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12
-  International Conference}, LNAI 814, pages 148--161. Springer, 1994.
-
-\bibitem{paulson-set-II}
-Lawrence~C. Paulson.
-\newblock Set theory for verification: {II}. {Induction} and recursion.
-\newblock {\em J. Auto. Reas.}, 15(2):167--215, 1995.
-
-\bibitem{paulson-generic}
-Lawrence~C. Paulson.
-\newblock Generic automatic proof tools.
-\newblock In Robert Veroff, editor, {\em Automated Reasoning and its
-  Applications: Essays in Honor of {Larry Wos}}, chapter~3. MIT Press, 1997.
-
-\bibitem{paulson-mscs}
-Lawrence~C. Paulson.
-\newblock Final coalgebras as greatest fixed points in zf set theory.
-\newblock {\em Mathematical Structures in Computer Science}, 9, 1999.
-\newblock in press.
-
-\bibitem{quaife92}
-Art Quaife.
-\newblock Automated deduction in {von Neumann-Bernays-G\"{o}del} set theory.
-\newblock {\em J. Auto. Reas.}, 8(1):91--147, 1992.
-
-\bibitem{suppes72}
-Patrick Suppes.
-\newblock {\em Axiomatic Set Theory}.
-\newblock Dover, 1972.
-
-\bibitem{principia}
-A.~N. Whitehead and B.~Russell.
-\newblock {\em Principia Mathematica}.
-\newblock Cambridge University Press, 1962.
-\newblock Paperback edition to *56, abridged from the 2nd edition (1927).
-
-\bibitem{winskel93}
-Glynn Winskel.
-\newblock {\em The Formal Semantics of Programming Languages}.
-\newblock MIT Press, 1993.
-
-\end{thebibliography}