doc-src/manual.bib

--- a/doc-src/manual.bib	Fri May 14 22:30:24 2010 +0200
+++ b/doc-src/manual.bib	Fri May 14 22:43:00 2010 +0200
@@ -228,13 +228,19 @@
 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
@@ -620,6 +626,11 @@
   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,
@@ -1256,6 +1267,15 @@
   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}
@@ -1287,6 +1307,15 @@
   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
@@ -1305,6 +1334,17 @@
   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
@@ -1411,6 +1451,11 @@
   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},
@@ -1750,6 +1795,14 @@
 %  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.}