@InProceedings{C4,
  key    =       {C04},
  author =	 {Christoph Benzm\"uller and Volker Sorge},
  title =	 {A Blackboard Architecture for Guiding Interactive Proofs},
  year =	 1998,
  editor =       {Fausto Giunchiglia}, 
  booktitle =	 {Artificial Intelligence: Methodology, Systems, and Applications,
               8th International Conference, AIMSA '98, Sozopol, Bulgaria, September
               21-13, 1998, Proceedings},
  series =	 {LNCS},
  number =       1480,
  pages =        {102--114},
  chrisnote =	 {C4},
  publisher =    {Springer},
  URL =		 {www.ags.uni-sb.de/~chris/papers/C4.pdf},
  abstract =	 {The acceptance and usability of current interactive theorem proving
                  environments is, among other things, strongly influenced by the
                  availability of an intelligent default suggestion mechanism for
                  commands. Such mechanisms support the user by decreasing the necessary
                  interactions during the proof construction. Although many systems offer
                  such facilities, they are often limited in their functionality. In this
                  paper we present a new agent-based mechanism that independently observes
                  the proof state, steadily computes suggestions on how to further
                  construct the proof, and communicates these suggestions to the user via
                  a graphical user interface. We furthermore introduce a focus technique
                  in order to restrict the search space when deriving default
                  suggestions. Although the agents we discuss in this paper are rather
                  simple from a computational viewpoint, we indicate how the presented
                  approach can be extended in order to increase its deductive power.}
}