Critical Agents Supporting Interactive Theorem Proving (bibtex)
by Christoph Benzmüller, Volker Sorge
Abstract:
We introduce a resource adaptive agent mechanism which supports the user in interactive theorem proving. The mechanism, an extension of \citeBeSo98b, uses a two layered architecture of agent societies to suggest appropriate commands together with possible command argument instantiations. Experiments with this approach show that its effectiveness can be further improved by introducing a resource concept. In this paper we provide an abstract view on the overall mechanism, motivate the necessity of an appropriate resource concept and discuss its realization within the agent architecture.
Reference:
Critical Agents Supporting Interactive Theorem Proving (Christoph Benzmüller, Volker Sorge), In Progress in Artificial Intelligence, 9th Portuguese Conference on Artificial Intelligence, EPIA '99, Évora, Portugal, September 21-24, 1999, Proceedings (Pedro Borahona, Jose J. Alferes, eds.), Springer, LNCS, number 1695, pp. 208-221, 1999. (slides) (Url (preprint): http://christoph-benzmueller.de/papers/C6.pdf)
Bibtex Entry:
@inproceedings{C6,
  Abstract =	 {We introduce a resource adaptive agent mechanism
                  which supports the user in interactive theorem
                  proving. The mechanism, an extension
                  of~\cite{BeSo98b}, uses a two layered architecture
                  of agent societies to suggest appropriate commands
                  together with possible command argument
                  instantiations. Experiments with this approach show
                  that its effectiveness can be further improved by
                  introducing a resource concept. In this paper we
                  provide an abstract view on the overall mechanism,
                  motivate the necessity of an appropriate resource
                  concept and discuss its realization within the agent
                  architecture.},
  Author =	 {Christoph Benzm{\"u}ller and Volker Sorge},
  Booktitle =	 {Progress in Artificial Intelligence, 9th Portuguese
                  Conference on Artificial Intelligence, EPIA '99,
                  {\'E}vora, Portugal, September 21-24, 1999,
                  Proceedings},
  Comment =	 {<a
                  href="http://christoph-benzmueller.de//papers/1999-epia-agents.pdf">slides</a>},
  Doi =		 {10.1007/3-540-48159-1_15},
  Editor =	 {Pedro Borahona and Jose J.~Alferes},
  Keywords =	 {own, Proof Assistants, OMEGA, Interactive Proof,
                  System Integration, Agents, LEO Prover},
  Number =	 1695,
  Pages =	 {208-221},
  Publisher =	 {Springer},
  Series =	 {LNCS},
  Title =	 {Critical Agents Supporting Interactive Theorem
                  Proving},
  Note =	 {Url (preprint):
                  \url{http://christoph-benzmueller.de/papers/C6.pdf}},
  Year =	 1999,
}
Powered by bibtexbrowser