Integrating TPS and OMEGA (bibtex)
by Christoph Benzmüller, Matt Bishop, Volker Sorge
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.
Reference:
Integrating TPS and OMEGA (Christoph Benzmüller, Matt Bishop, Volker Sorge), In Journal of Universal Computer Science, volume 5, number 3, pp. 188-207, 1999. (Url (preprint): http://christoph-benzmueller.de/papers/J1.pdf)
Bibtex Entry:
@article{J1,
  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.},
  Author =	 {Christoph Benzm{\"u}ller and Matt Bishop and Volker
                  Sorge},
  Doi =		 {10.3217/jucs-005-03-0188},
  Journal =	 {Journal of Universal Computer Science},
  Keywords =	 {own, Proof Assistants, OMEGA, Proof Transformation,
                  System Integration, Higher Order Logic},
  Number =	 3,
  Pages =	 {188-207},
  Title =	 {Integrating {TPS} and {OMEGA}},
  Note =	 {Url (preprint):
                  \url{http://christoph-benzmueller.de/papers/J1.pdf}},
  Volume =	 5,
  Year =	 1999,
}
Powered by bibtexbrowser