Integrating TPS with OMEGA (bibtex)

by Christoph Benzmüller, Volker Sorge

Abstract:

We report on the integration of TPS as an external reasoning component into the mathematical assistant system OMEGA. Thereby TPS can be used both as an automatic theorem prover for higher order logic as well as interactively employed from within the OMEGA environment. TPS proofs can be directly incorporated into OMEGA on a tactic level enabling their visualization and verbalization. Using an example we show how \tps\/ proofs can be inserted into OMEGA's knowledge base by expanding them to calculus level using both OMEGA's tactic mechanism and the first order theorem prover OTTER. Furthermore we demonstrate how the facts from OMEGA's knowledge base can be used to build a TPS library.

Reference:

Integrating TPS with OMEGA (Christoph Benzmüller, Volker Sorge), In Theorem Proving in Higher Order Logics: Emerging Trends (Jim Grundy, Malcolm Newey, eds.), Technical Report 98-08, Department of Computer Science and Computer Science Lab, The Australian National University, pp. 1-18, 1998. (Url (preprint): http://christoph-benzmueller.de/papers/W2.pdf)

Bibtex Entry:

@inproceedings{W2, Abstract = {We report on the integration of TPS as an external reasoning component into the mathematical assistant system OMEGA. Thereby TPS can be used both as an automatic theorem prover for higher order logic as well as interactively employed from within the OMEGA environment. TPS proofs can be directly incorporated into OMEGA on a tactic level enabling their visualization and verbalization. Using an example we show how \tps\/ proofs can be inserted into OMEGA's knowledge base by expanding them to calculus level using both OMEGA's tactic mechanism and the first order theorem prover OTTER. Furthermore we demonstrate how the facts from OMEGA's knowledge base can be used to build a TPS library.}, Address = {Canberra, Australia}, Author = {Christoph Benzm{\"u}ller and Volker Sorge}, Booktitle = {Theorem Proving in Higher Order Logics: Emerging Trends}, Editor = {Jim Grundy and Malcolm Newey}, Keywords = {own, Proof Assistants, OMEGA, Interactive Proof, Proof Transformation, System Integration}, Pages = {1-18}, Series = {Technical Report 98-08, Department of Computer Science and Computer Science Lab, The Australian National University}, Title = {Integrating {TPS} with {OMEGA}}, Note = {Url (preprint): \url{http://christoph-benzmueller.de/papers/W2.pdf}}, Year = 1998, }

Powered by bibtexbrowser