A Blackboard Architecture for Guiding Interactive Proofs (bibtex)
by Christoph Benzmüller, Volker Sorge
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.
Reference:
A Blackboard Architecture for Guiding Interactive Proofs (Christoph Benzmüller, Volker Sorge), In Artificial Intelligence: Methodology, Systems, and Applications, 8th International Conference, AIMSA '98, Sozopol, Bulgaria, September 21-13, 1998, Proceedings (Fausto Giunchiglia, ed.), Springer, LNCS, number 1480, pp. 102-114, 1998. (Url (preprint): http://christoph-benzmueller.de/papers/C4.pdf)
Bibtex Entry:
@inproceedings{C4,
  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.},
  Author =	 {Christoph Benzm\"uller and Volker Sorge},
  Booktitle =	 {Artificial Intelligence: Methodology, Systems, and
                  Applications, 8th International Conference, AIMSA
                  '98, Sozopol, Bulgaria, September 21-13, 1998,
                  Proceedings},
  Doi =		 {10.1007/BFb0057438},
  Editor =	 {Fausto Giunchiglia},
  Keywords =	 {own, Proof Assistants, OMEGA, Interactive Proof,
                  System Integration, Agents},
  Number =	 1480,
  Pages =	 {102-114},
  Publisher =	 {Springer},
  Series =	 {LNCS},
  Title =	 {A Blackboard Architecture for Guiding Interactive
                  Proofs},
  Note =	 {Url (preprint):
                  \url{http://christoph-benzmueller.de/papers/C4.pdf}},
  Year =	 1998,
}
Powered by bibtexbrowser