Shared tools and models problem -- sharing basic theories

Interactive theorem provers require large libraries of formalized mathematics to be effective. Building them is very time consuming and labor intensive, yet every theorem proving research group reproves basic facts that other groups have already done, especially numerical facts-for N, Z, Q, or the reals R, also theories of lists, trees, graphs, automata and other basic data types and models.

An obvious approach to avoid this costly duplication is to share a data base of basic facts. It turns out that doing this is difficult. A great deal of theory has been directed toward elegant solutions [], but it is not clear what is practical. The difficulties are that mathematics is represented slightly differently in all systems, in older systems there are very idosyncratic definitions, even of the natural numbers! Systems use different logics and different primitive notions. The provers can store state with the facts.

Despite these problems, we have shown that it is possible to share results between two major interactive provers based on very different logics but sharing the same theorem proving style, namely HOL and Nuprl can share. Not only this, PVS is the same type of prover, so sharing with it seems very plausible as we propose to show.

So while we expect that there will always be several major verification systems, some in industry, some in academia, some in Europe, etc., and while they will need to develop their own specialized theories, it is possible for them to share a large core of basic mathematics.

The model we envision is shown in Figure 1. All mathematics is exchanged over a common channel, called MathBus ; the logical library serves as a formal knowledge base for the mathematics from the heterogenous systems; the logical environment provides organization of results in the library; and logic editors are used to view the mathematics in the system. Each of the components is part of the research we are proposing.

  

Figure 1: Logical Programming Environment