**Author:** Julian Backes
**Advisor:** Dr. Chad E. Brown
**Supervisor:** Professor Dr. Gert Smolka

- Download thesis
- Final Talk: Monday, April 06, 2009, 14:15. Building E1.3, Room 825 (download slides)
- 12.12.2008 14:00 ct.: Proposal talk (download slides)
- 21.11.2008 14:00 ct.: First talk (download slides)

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.

- G. Sutcliffe, C. Suttner:
**TPTP: Thousands of Problems for Theorem Provers**

http://www.tptp.org/ - Christoph Benzmueller, Florian Rabe, Geoff Suttcliffe.
**The Core TPTP Language for Classical Higher-Order Logic**. IJCAR'08. To appear. - William M. Farmer, Joshua D. Guttman, F. Javier Thayer.
**Little theories**. Proceedings of the 11th International Conference on Automated Deduction (CADE 11). 567--581, 1992. - Dieter Hutter.
**Management of change in structured verification**. In Proceedings 15th IEEE International Conference on Automated Software Engineering, number 2000 in ASE. 23--34, 2000. - R.M. Burstall, J.A. Goguen:
**Putting theories together to make specifications**(1977) - J.A. Goguen, R.M. Burstall:
**Institutions: Abstract Model Theory for Specification and Programming**(1992)

http://www.cs.ucsd.edu/~goguen/projs/inst.html - W.M. Farmer, J.D. Guttman, F.J. Thayer:
**IMPS: An Interactive Mathematical Proof System**(1993) - G. Smolka, C.E. Brown:
**Introduction to Computational Logic. Lecture Notes SS 2008**(2008)