Agent-based Proof Search with Indexed Formulas (bibtex)

by Malte Hübner, Serge Autexier, Christoph Benzmüller

Abstract:

This paper describes work aimed at integrating OMEGA's agent-based suggestion mechanism OANTS and the new theorem proving framework developed by Autexier [Autexier01].

Reference:

Agent-based Proof Search with Indexed Formulas (Malte Hübner, Serge Autexier, Christoph Benzmüller), In Additonal Proceedings of 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS 2002), pp. 11-20, 2002. (slides) (Preprint: http://christoph-benzmueller.de/papers/W16.pdf)

Bibtex Entry:

@inproceedings{W16, Abstract = {This paper describes work aimed at integrating OMEGA's agent-based suggestion mechanism OANTS and the new theorem proving framework developed by Autexier [Autexier01].}, Address = {Marseilles, France}, Author = {Malte H{\"u}bner and Serge Autexier and Christoph Benzm{\"u}ller}, Booktitle = {Additonal Proceedings of 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS 2002)}, Comment = {<a href="http://christoph-benzmueller.de//papers/2002-calculemus-talk.pdf">slides</a>}, Pages = {11-20}, Title = {Agent-based Proof Search with Indexed Formulas}, Addendum = {Preprint: \url{http://christoph-benzmueller.de/papers/W16.pdf}}, Year = 2002, }