OANTS -- Combining Interactive and Automated Theorem Proving (bibtex)

by Christoph Benzmüller, Volker Sorge

Abstract:

We present the O-ANTS theorem prover that is built on top of an agent-based command suggestion mechanism. The theorem prover inherits beneficial properties from the underlying suggestion mechanism such as run-time extendibility and resource adaptability. Moreover, it supports the distributed integration of external reasoning systems. We also discuss how the implementation and modeling of a calculus in our agent-based approach can be investigated wrt. the inheritance of properties such as completeness and soundness.

Reference:

OANTS -- Combining Interactive and Automated Theorem Proving (Christoph Benzmüller, Volker Sorge), In Symbolic Computation and Automated Reasoning (Manfred Kerber, Michael Kohlhase, eds.), A.K.Peters, pp. 81-97, 2001. (slides) (Preprint: http://christoph-benzmueller.de/papers/C8.pdf)

Bibtex Entry:

@inproceedings{C8, Abstract = {We present the O-ANTS theorem prover that is built on top of an agent-based command suggestion mechanism. The theorem prover inherits beneficial properties from the underlying suggestion mechanism such as run-time extendibility and resource adaptability. Moreover, it supports the distributed integration of external reasoning systems. We also discuss how the implementation and modeling of a calculus in our agent-based approach can be investigated wrt. the inheritance of properties such as completeness and soundness.}, Author = {Christoph Benzm{\"u}ller and Volker Sorge}, Booktitle = {Symbolic Computation and Automated Reasoning}, Comment = {<a href="http://christoph-benzmueller.de//papers/2000-calculemus-oants.pdf">slides</a>}, Editor = {Manfred Kerber and Michael Kohlhase}, Keywords = {own, Proof Assistants, OMEGA, Interactive Proof, Automated Reasoning, System Integration, Agents, LEO Prover}, Pages = {81-97}, Publisher = {A.K.Peters}, Title = {{OANTS} -- Combining Interactive and Automated Theorem Proving}, Addendum = {Preprint: \url{http://christoph-benzmueller.de/papers/C8.pdf}}, Year = 2001, }