@Article{J1,
  key    =       {J01},
  author =	 {Christoph Benzm{\"u}ller and Matt Bishop and Volker Sorge},
  title =	 {Integrating {TPS} and {OMEGA}},
  journal =	 {Journal of Universal Computer Science},
  year =	 1999,
  volume =	 5,
  number =	 3,
  pages =	 {188--207},
  url =		 {www.ags.uni-sb.de/~chris/papers/J1.pdf},
  abstract =	 {This paper reports on the integration of the higher-order theorem
                  proving environment TPS [Andrews96] into the mathematical assistant
                  OMEGA [Omega97]. TPS can be called from OMEGA either as a black box or
                  as an interactive system. In black box mode, the user has control over
                  the parameters which control proof search in TPS; in interactive mode,
                  all features of the TPS-system are available to the user. If the
                  subproblem which is passed to TPS contains concepts defined in OMEGA's
                  database of mathematical theories, these definitions are not
                  instantiated but are also passed to TPS. Using a special theory which
                  contains proof tactics that model the ND-calculus variant of TPS within
                  OMEGA, any complete or partial proof generated in TPS can be translated
                  one to one into an OMEGA proof plan. Proof transformation is realised by
                  proof plan expansion in OMEGA's 3-dimensional proof data structure, and
                  remains transparent to the user.},
  note = {doi:10.3217/jucs-005-03-0188},
  chrisnote =	 {J1}
}