]> matita.cs.unibo.it Git - helm.git/commitdiff
A new references.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 29 May 2003 12:26:57 +0000 (12:26 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 29 May 2003 12:26:57 +0000 (12:26 +0000)
helm/papers/calculemus-2003/hbugs-calculemus-2003.tex

index 66ada2b98969f92815dcd170e86f51e33b4e50e3..9e3db7894a8cb73d65cb0a71815fce7e20e56fad 100644 (file)
   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.