doc-src/ZF/logics-ZF.bbl
changeset 6121 5fe77b9b5185
child 6592 c120262044b6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/ZF/logics-ZF.bbl	Wed Jan 13 16:36:36 1999 +0100
     1.3 @@ -0,0 +1,124 @@
     1.4 +\begin{thebibliography}{10}
     1.5 +
     1.6 +\bibitem{abrial93}
     1.7 +J.~R. Abrial and G.~Laffitte.
     1.8 +\newblock Towards the mechanization of the proofs of some classical theorems of
     1.9 +  set theory.
    1.10 +\newblock preprint, February 1993.
    1.11 +
    1.12 +\bibitem{basin91}
    1.13 +David Basin and Matt Kaufmann.
    1.14 +\newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison.
    1.15 +\newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical
    1.16 +  Frameworks}, pages 89--119. Cambridge University Press, 1991.
    1.17 +
    1.18 +\bibitem{boyer86}
    1.19 +Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and
    1.20 +  Lawrence Wos.
    1.21 +\newblock Set theory in first-order logic: Clauses for {G\"{o}del's} axioms.
    1.22 +\newblock {\em Journal of Automated Reasoning}, 2(3):287--327, 1986.
    1.23 +
    1.24 +\bibitem{camilleri92}
    1.25 +J.~Camilleri and T.~F. Melham.
    1.26 +\newblock Reasoning with inductively defined relations in the {HOL} theorem
    1.27 +  prover.
    1.28 +\newblock Technical Report 265, Computer Laboratory, University of Cambridge,
    1.29 +  August 1992.
    1.30 +
    1.31 +\bibitem{davey&priestley}
    1.32 +B.~A. Davey and H.~A. Priestley.
    1.33 +\newblock {\em Introduction to Lattices and Order}.
    1.34 +\newblock Cambridge University Press, 1990.
    1.35 +
    1.36 +\bibitem{devlin79}
    1.37 +Keith~J. Devlin.
    1.38 +\newblock {\em Fundamentals of Contemporary Set Theory}.
    1.39 +\newblock Springer, 1979.
    1.40 +
    1.41 +\bibitem{dummett}
    1.42 +Michael Dummett.
    1.43 +\newblock {\em Elements of Intuitionism}.
    1.44 +\newblock Oxford University Press, 1977.
    1.45 +
    1.46 +\bibitem{dyckhoff}
    1.47 +Roy Dyckhoff.
    1.48 +\newblock Contraction-free sequent calculi for intuitionistic logic.
    1.49 +\newblock {\em Journal of Symbolic Logic}, 57(3):795--807, 1992.
    1.50 +
    1.51 +\bibitem{halmos60}
    1.52 +Paul~R. Halmos.
    1.53 +\newblock {\em Naive Set Theory}.
    1.54 +\newblock Van Nostrand, 1960.
    1.55 +
    1.56 +\bibitem{kunen80}
    1.57 +Kenneth Kunen.
    1.58 +\newblock {\em Set Theory: An Introduction to Independence Proofs}.
    1.59 +\newblock North-Holland, 1980.
    1.60 +
    1.61 +\bibitem{noel}
    1.62 +Philippe No{\"e}l.
    1.63 +\newblock Experimenting with {Isabelle} in {ZF} set theory.
    1.64 +\newblock {\em Journal of Automated Reasoning}, 10(1):15--58, 1993.
    1.65 +
    1.66 +\bibitem{paulin92}
    1.67 +Christine Paulin-Mohring.
    1.68 +\newblock Inductive definitions in the system {Coq}: Rules and properties.
    1.69 +\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon,
    1.70 +  December 1992.
    1.71 +
    1.72 +\bibitem{paulson87}
    1.73 +Lawrence~C. Paulson.
    1.74 +\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
    1.75 +\newblock Cambridge University Press, 1987.
    1.76 +
    1.77 +\bibitem{paulson-set-I}
    1.78 +Lawrence~C. Paulson.
    1.79 +\newblock Set theory for verification: {I}. {From} foundations to functions.
    1.80 +\newblock {\em Journal of Automated Reasoning}, 11(3):353--389, 1993.
    1.81 +
    1.82 +\bibitem{paulson-CADE}
    1.83 +Lawrence~C. Paulson.
    1.84 +\newblock A fixedpoint approach to implementing (co)inductive definitions.
    1.85 +\newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12
    1.86 +  International Conference}, LNAI 814, pages 148--161. Springer, 1994.
    1.87 +
    1.88 +\bibitem{paulson-final}
    1.89 +Lawrence~C. Paulson.
    1.90 +\newblock A concrete final coalgebra theorem for {ZF} set theory.
    1.91 +\newblock In Peter Dybjer, Bengt Nordstr{\"om}, and Jan Smith, editors, {\em
    1.92 +  Types for Proofs and Programs: International Workshop {TYPES '94}}, LNCS 996,
    1.93 +  pages 120--139. Springer, 1995.
    1.94 +
    1.95 +\bibitem{paulson-set-II}
    1.96 +Lawrence~C. Paulson.
    1.97 +\newblock Set theory for verification: {II}. {Induction} and recursion.
    1.98 +\newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
    1.99 +
   1.100 +\bibitem{paulson-generic}
   1.101 +Lawrence~C. Paulson.
   1.102 +\newblock Generic automatic proof tools.
   1.103 +\newblock In Robert Veroff, editor, {\em Automated Reasoning and its
   1.104 +  Applications: Essays in Honor of {Larry Wos}}, chapter~3. MIT Press, 1997.
   1.105 +
   1.106 +\bibitem{quaife92}
   1.107 +Art Quaife.
   1.108 +\newblock Automated deduction in {von Neumann-Bernays-G\"{o}del} set theory.
   1.109 +\newblock {\em Journal of Automated Reasoning}, 8(1):91--147, 1992.
   1.110 +
   1.111 +\bibitem{suppes72}
   1.112 +Patrick Suppes.
   1.113 +\newblock {\em Axiomatic Set Theory}.
   1.114 +\newblock Dover, 1972.
   1.115 +
   1.116 +\bibitem{principia}
   1.117 +A.~N. Whitehead and B.~Russell.
   1.118 +\newblock {\em Principia Mathematica}.
   1.119 +\newblock Cambridge University Press, 1962.
   1.120 +\newblock Paperback edition to *56, abridged from the 2nd edition (1927).
   1.121 +
   1.122 +\bibitem{winskel93}
   1.123 +Glynn Winskel.
   1.124 +\newblock {\em The Formal Semantics of Programming Languages}.
   1.125 +\newblock MIT Press, 1993.
   1.126 +
   1.127 +\end{thebibliography}