doc-src/Logics/logics.bbl
changeset 1399 1f00494e37a5
parent 1054 f3fabffd927a
child 1444 23ceb1dc9755
equal deleted inserted replaced
1398:b8de98c2c29c 1399:1f00494e37a5
    71 \bibitem{felty91a}
    71 \bibitem{felty91a}
    72 Amy Felty.
    72 Amy Felty.
    73 \newblock A logic program for transforming sequent proofs to natural deduction
    73 \newblock A logic program for transforming sequent proofs to natural deduction
    74   proofs.
    74   proofs.
    75 \newblock In Peter Schroeder-Heister, editor, {\em Extensions of Logic
    75 \newblock In Peter Schroeder-Heister, editor, {\em Extensions of Logic
    76   Programming}, pages 157--178. Springer, 1991.
    76   Programming}, LNAI 475, pages 157--178. Springer, 1991.
    77 \newblock LNAI 475.
       
    78 
    77 
    79 \bibitem{frost93}
    78 \bibitem{frost93}
    80 Jacob Frost.
    79 Jacob Frost.
    81 \newblock A case study of co-induction in {Isabelle HOL}.
    80 \newblock A case study of co-induction in {Isabelle HOL}.
    82 \newblock Technical Report 308, Computer Laboratory, University of Cambridge,
    81 \newblock Technical Report 308, Computer Laboratory, University of Cambridge,
   112 
   111 
   113 \bibitem{alf}
   112 \bibitem{alf}
   114 Lena Magnusson and Bengt {Nordstr\"om}.
   113 Lena Magnusson and Bengt {Nordstr\"om}.
   115 \newblock The {ALF} proof editor and its proof engine.
   114 \newblock The {ALF} proof editor and its proof engine.
   116 \newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
   115 \newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
   117   '93}}, pages 213--237. Springer, published 1994.
   116   '93}}, LNCS 806, pages 213--237. Springer, published 1994.
   118 \newblock LNCS 806.
       
   119 
   117 
   120 \bibitem{mw81}
   118 \bibitem{mw81}
   121 Zohar Manna and Richard Waldinger.
   119 Zohar Manna and Richard Waldinger.
   122 \newblock Deductive synthesis of the unification algorithm.
   120 \newblock Deductive synthesis of the unification algorithm.
   123 \newblock {\em Science of Computer Programming}, 1(1):5--48, 1981.
   121 \newblock {\em Science of Computer Programming}, 1(1):5--48, 1981.
   168 \bibitem{paulson-coind}
   166 \bibitem{paulson-coind}
   169 Lawrence~C. Paulson.
   167 Lawrence~C. Paulson.
   170 \newblock Co-induction and co-recursion in higher-order logic.
   168 \newblock Co-induction and co-recursion in higher-order logic.
   171 \newblock Technical Report 304, Computer Laboratory, University of Cambridge,
   169 \newblock Technical Report 304, Computer Laboratory, University of Cambridge,
   172   July 1993.
   170   July 1993.
       
   171 \newblock To appear in the Festscrift for Alonzo Church, edited by A. Anderson
       
   172   and M. Zeleny.
   173 
   173 
   174 \bibitem{paulson-set-I}
   174 \bibitem{paulson-set-I}
   175 Lawrence~C. Paulson.
   175 Lawrence~C. Paulson.
   176 \newblock Set theory for verification: {I}. {From} foundations to functions.
   176 \newblock Set theory for verification: {I}. {From} foundations to functions.
   177 \newblock {\em Journal of Automated Reasoning}, 11(3):353--389, 1993.
   177 \newblock {\em Journal of Automated Reasoning}, 11(3):353--389, 1993.
   178 
   178 
   179 \bibitem{paulson-set-II}
       
   180 Lawrence~C. Paulson.
       
   181 \newblock Set theory for verification: {II}. {Induction} and recursion.
       
   182 \newblock Technical Report 312, Computer Laboratory, University of Cambridge,
       
   183   1993.
       
   184 \newblock To appear in Journal of Automated Reasoning.
       
   185 
       
   186 \bibitem{paulson-final}
       
   187 Lawrence~C. Paulson.
       
   188 \newblock A concrete final coalgebra theorem for {ZF} set theory.
       
   189 \newblock Technical Report 334, Computer Laboratory, University of Cambridge,
       
   190   1994.
       
   191 
       
   192 \bibitem{paulson-CADE}
   179 \bibitem{paulson-CADE}
   193 Lawrence~C. Paulson.
   180 Lawrence~C. Paulson.
   194 \newblock A fixedpoint approach to implementing (co)inductive definitions.
   181 \newblock A fixedpoint approach to implementing (co)inductive definitions.
   195 \newblock In Alan Bundy, editor, {\em 12th International Conference on
   182 \newblock In Alan Bundy, editor, {\em 12th International Conference on
   196   Automated Deduction}, pages 148--161. Springer, 1994.
   183   Automated Deduction}, LNAI 814, pages 148--161. Springer, 1994.
   197 \newblock LNAI 814.
   184 
       
   185 \bibitem{paulson-set-II}
       
   186 Lawrence~C. Paulson.
       
   187 \newblock Set theory for verification: {II}. {Induction} and recursion.
       
   188 \newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
   198 
   189 
   199 \bibitem{paulson-COLOG}
   190 \bibitem{paulson-COLOG}
   200 Lawrence~C. Paulson.
   191 Lawrence~C. Paulson.
   201 \newblock A formulation of the simple theory of types (for {Isabelle}).
   192 \newblock A formulation of the simple theory of types (for {Isabelle}).
   202 \newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88:
   193 \newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88:
   203   International Conference on Computer Logic}, pages 246--274, Tallinn,
   194   International Conference on Computer Logic}, LNCS 417, pages 246--274,
   204   Published 1990. Estonian Academy of Sciences, Springer.
   195   Tallinn, Published 1990. Estonian Academy of Sciences, Springer.
   205 \newblock LNCS 417.
   196 
       
   197 \bibitem{paulson-final}
       
   198 Lawrence~C. Paulson.
       
   199 \newblock A concrete final coalgebra theorem for {ZF} set theory.
       
   200 \newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
       
   201   '94}}, LNCS 996, pages 120--139. Springer, published 1995.
   206 
   202 
   207 \bibitem{pelletier86}
   203 \bibitem{pelletier86}
   208 F.~J. Pelletier.
   204 F.~J. Pelletier.
   209 \newblock Seventy-five problems for testing automatic theorem provers.
   205 \newblock Seventy-five problems for testing automatic theorem provers.
   210 \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
   206 \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.