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) (Url (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},
  Note =	 {Url (preprint):
                  \url{http://christoph-benzmueller.de/papers/C8.pdf}},
  Year =	 2001,
}
Powered by bibtexbrowser