X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita.bib;fp=helm%2Fpapers%2Fmatita%2Fmatita.bib;h=7d98905d56e5ff0b6833e5df58753c6a6fee2b1a;hb=ed308fc03be5397081ac0e00bbc73b3f71da1e67;hp=8aa1c4882a5aecce42eec255e484ab6d85b44031;hpb=c051f623926cdc3b744c38ba393c0a9c7622d299;p=helm.git

diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib
index 8aa1c4882..7d98905d5 100644
--- a/helm/papers/matita/matita.bib
+++ b/helm/papers/matita/matita.bib
@@ -1,3 +1,12 @@
+@inproceedings{paramodulation,
+  author = "Robert Nieuwenhuis and Alberto Rubio",
+  title = "Paramodulation-based thorem proving",
+  booktitle = "Handbook of Automated Reasoning",
+  editor = "John Alan Robinson and Andrei Voronkov",
+  pages = "471--443",
+  publisher = "Elsevier and MIT Press",
+  year = 2001,
+}
 
 @inproceedings{latexmathml,
  author = {Luca Padovani},