In this contribution we propose an agent architecture for theorem proving which we intend to investigate in depth in the future. The work reported in this paper is in an early state, and by no means finished. We present and discuss our proposal in order to get feedback from the Calculemus community.

Accessing knowledge of a single knowledge source with different client applications often requires the help of mediator systems as middleware components. In the domain of theorem proving large efforts have been made to formalize knowledge for mathematics and verification issues, and to structure it in databases. But these databases are either specialized for a single client, or if the knowledge is stored in a general database, the services this database can provide are usually limited and hard to adjust for a (...) particular theorem prover. Only recently there have been initiatives to flexibly connect existing theorem proving systems into networked environments that contain large knowledge bases. An intermediate layer containing both, search and proving functionality can be used to mediate between the two. In this paper we motivate the need and discuss the requirements for mediators between mathematical knowledge bases and theorem proving systems. We also present an attempt at a concurrent mediator between a knowledge base and a proof planning system. (shrink)

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. (shrink)

Twenty-four critical essays, including a substantial introduction, written by the most distinguished international scholars, in honour of Graziella Federici Vescovini.