From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 29 May 2003 12:26:57 +0000 (+0000)
Subject: A new references.
X-Git-Tag: submitted~17
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=60bc0c5ad2b5b0146bca7f7c6dd5633b0a1e3498;p=helm.git

A new references.
---

diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
index 66ada2b98..9e3db7894 100644
--- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
+++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
@@ -112,8 +112,8 @@
   mathematical entities; the Getter plays the role of the Mathematical Object
   Manager in the MONET framework.
 
-  A precursor of \hbugs{} is the \OmegaAnts{} project \cite{omegaants},
-  which provided similar functionalities to the
+  A precursor of \hbugs{} is the \OmegaAnts{} project
+  \cite{omegaants1,omegaants2}, which provided similar functionalities to the
   \Omegapp{} proof-planner \cite{omega}. The main architectural difference
   between \hbugs{} and \OmegaAnts{} are that the latter is based on a
   black-board architecture and it is not implemented using \wss{} and
@@ -696,7 +696,12 @@ we have investigated three classes of tutors:
  Mathematical Knowledge Management in HELM. In Annals of Mathematics and
  Artificial Intelligence, 38(1): 27--46, May 2003.
 
-\bibitem{omegaants} C. Benzm\"uller, M. Jamnik, M. Kerber, V. Sorge.
+\bibitem{omegaants1} C. Benzm\"uller, V. Sorge. O-Ants -- An Open Approach
+ at Combining Interactive and Automated Theorem Proving. In M. Kerber and
+ M. Kohlhase (eds.), Integration of Symbolic and Mechanized Reasoning, pp.
+ 81--97, 2000.
+
+\bibitem{omegaants2} C. Benzm\"uller, M. Jamnik, M. Kerber, V. Sorge.
  Agent-based Mathematical Reasoning. In A. Armando and T. Jebelean (eds.),
  Electronic Notes in Theoretical Computer Science, (1999) 23(3), Elsevier.