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