Author: Julian Backes
Advisor: Dr. Chad E. Brown
Supervisor: Professor Dr. Gert Smolka
Jitpro is an interactive theorem prover for higher-order logic. At the moment, one specifies the theorem to prove by giving a number of sorts, constants, definitions, axioms and some claims. Clearly many different specifications will make use of common basic elements. For example, many specifications may make use of the definition of the union between two sets. There should be a mechanism to allow constructing a problem specification by importing a number of other specifications. The import mechanism will need to take care of potential name conflicts and allow for instantiations for basic sorts and constants during importing.
A similar problem is that of retrieving definitions, axioms and claims which have been specified earlier. Retrieving higher-order terms can be a very difficult problem since higher-order unification is undecidable. In this project we want a relatively simple retrieval mechanism which avoids higher-order unification and higher-order matching.
Once one has a specification (possibly obtained by importing smaller specifications), one should be able to present the specification in a variety of forms. Primarily we want to have the specification as a problem file for Jitpro. We would also like to be able to present the specification as documentation of itself (e.g., in the form of a web page). We should also output particular claims in the specification in THF syntax for the new higher-order TPTP library.
The goal of this project is to design a system for storing, retrieving, combining and presenting higher-order specifications. Using the system, one should be able to store specifications, combine specifications to make a larger specification, search for definitions, axioms and claims, and extract specifications in various forms giving a problem specification for Jitpro, documentation (as a web page), and a THF problem specification for the TPTP.