doc-src/manual.bib

 
 @book{Bird-Haskell,author="Richard Bird",
 title="Introduction to Functional Programming using Haskell",
 publisher=PH,year=1998}
 
-@inproceedings{blanchette-nipkow-2009,
-  title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder (Extended Abstract)",
+@inproceedings{blanchette-nipkow-2010,
+  title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder",
   author = "Jasmin Christian Blanchette and Tobias Nipkow",
-  booktitle = "{TAP} 2009: Short Papers",
-  editor = "Catherine Dubois",
-  publisher = "ETH Technical Report 630",
-  year = 2009}
+  crossref = {itp2010}}
+
+@inproceedings{boehme-nipkow-2010,
+  author={Sascha B\"ohme and Tobias Nipkow},
+  title={Sledgehammer: Judgement Day},
+  booktitle={Automated Reasoning: IJCAR 2010},
+  editor={J. Giesl and R. H\"ahnle},
+  publisher=Springer,
+  series=LNCS,
+  year=2010}
 
 @Article{boyer86,
   author	= {Robert Boyer and Ewing Lusk and William McCune and Ross
 		   Overbeek and Mark Stickel and Lawrence Wos},
   title		= {Set Theory in First-Order Logic: Clauses for {G\"{o}del's}

 @InProceedings{Harrison:1996:MizarHOL,
   author = 	 {J. Harrison},
   title = 	 {A {Mizar} Mode for {HOL}},
   pages =	 {203--220},
   crossref =     {tphols96}}
+
+@misc{metis,
+  author = "Joe Hurd",
+  title = "Metis Theorem Prover",
+  note = "\url{http://www.gilith.com/software/metis/}"}
 
 %J
 
 @article{haskell-revised-report,
   author =  {Simon {Peyton Jones} and others},

   author	= {Steve Reeves and Michael Clarke},
   title		= {Logic for Computer Science},
   publisher	= {Addison-Wesley},
   year		= 1990}
 
+@article{riazanov-voronkov-2002,
+  author = "Alexander Riazanov and Andrei Voronkov",
+  title = "The Design and Implementation of {Vampire}",
+  journal = "Journal of AI Communications",
+  year = 2002,
+  volume = 15,
+  number ="2/3",
+  pages = "91--110"}
+
 @book{Rosen-DMA,author={Kenneth H. Rosen},
 title={Discrete Mathematics and Its Applications},
 publisher={McGraw-Hill},year=1998}
 
 @InProceedings{Rudnicki:1992:MizarOverview,

   year =         1984,
   volume =       49,
   number =       4
 }
 
+@article{schulz-2002,
+  author = "Stephan Schulz",
+  title = "E---A Brainiac Theorem Prover",
+  journal = "Journal of AI Communications",
+  year = 2002,
+  volume = 15,
+  number ="2/3",
+  pages = "111--126"}
+
 @misc{sledgehammer-2009,
   key = "Sledgehammer",
   title = "The {S}ledgehammer: Let Automatic Theorem Provers
 Write Your {I}s\-a\-belle Scripts",
   note = "\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/sledgehammer.html}"}

 @book{suppes72,
   author	= {Patrick Suppes},
   title		= {Axiomatic Set Theory},
   year		= 1972,
   publisher	= {Dover}}
+
+@inproceedings{sutcliffe-2000,
+  author = "Geoff Sutcliffe",
+  title = "System Description: {SystemOnTPTP}",
+  editor = "J. G. Carbonell and J. Siekmann",
+  booktitle	= {Automated Deduction --- {CADE}-17 International Conference},
+  series = "Lecture Notes in Artificial Intelligence",
+  volume = {1831},
+  pages = "406--410",
+  year = 2000,
+  publisher = Springer}
 
 @InCollection{szasz93,
   author	= {Nora Szasz},
   title		= {A Machine Checked Proof that {Ackermann's} Function is not
 		  Primitive Recursive},

   author =	 {Christoph Wedler},
   title =	 {Emacs package ``{X-Symbol}''},
   note =	 {\url{http://x-symbol.sourceforge.net}}
 }
 
+@misc{weidenbach-et-al-2009,
+  author = "Christoph Weidenbach and Dilyana Dimova and Arnaud Fietzke and Rohit Kumar and Martin Suda and Patrick Wischnewski",
+  title = "{SPASS} Version 3.5",
+  note = {\url{http://www.spass-prover.org/publications/spass.pdf}}}
+
 @manual{isabelle-sys,
   author	= {Markus Wenzel and Stefan Berghofer},
   title		= {The {Isabelle} System Manual},
   institution	= {TU Munich},
   note          = {\url{http://isabelle.in.tum.de/doc/system.pdf}}}

   series        = LNCS,
   year          = 2008}
 %  editor        =
 %  volume        = 4732,
 
+@Proceedings{itp2010,
+  title         = {Interactive Theorem Proving: {ITP}-10},
+  booktitle     = {Interactive Theorem Proving: {ITP}-10},
+  editor = "Matt Kaufmann and Lawrence Paulson",
+  publisher     = Springer,
+  series        = LNCS,
+  year          = 2010}
+
 @unpublished{classes_modules,
   title         = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison},
   author        = {Stefan Wehr et. al.}
 }