@INPROCEEDINGS{W2,
  key    =       {W02},
  AUTHOR =	 {Christoph Benzm{\"u}ller and Volker Sorge},
  TITLE =	 {Integrating {\sc Tps} with {$\Omega$\sc mega}},
  BOOKTITLE =	 {Theorem Proving in Higher Order Logics: Emerging Trends},
  EDITOR =	 {Jim Grundy and Malcolm Newey},
  ADDRESS =	 {Canberra, Australia},
  MONTH =	 {October},
  YEAR =	 1998,
  PAGES =	 {1--18},
  CHRISNOTE =	 {W2},
  SERIES =	 {Technical Report 98-08, Department of Computer Science and Computer
                  Science Lab, The Australian National University},
  URL =		 {www.ags.uni-sb.de/~chris/papers/W2.pdf},
  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.}
}