Synthetic Philosophy and Deductive Engineering
The ProofPower HOL system has a library of theories, which is a good first candidate for initial population of a SPaDE repository, and will serve as a basis for early prototyping of the SPaDE knowledge repository and the SPaDE MCP server. Even larger libraries exist for other ITP systems, such as HOL4 and Lean, and these may be considered for import into SPaDE as the project progresses.
This document describes the process of extracting the content of the ProofPower HOL library into a SPaDE native repository.
The ProofPower HOL system is implemented in Standard ML. The theory hierarchy is stored in a PolyML database, and the system provides an API for accessing that database. This document is primarily concerned with implementation of a procedure in SML which extracts the content of that database and writes it out in the SPaDE native repository format.
The SPaDE repository is summarised in README.md.
A HOL4 specification of the abstract syntax of the SPaDE repository is given in krcd006.sml.
The core ProofPower export program is implemented in krcd005.sml.
The Python tooling for interacting with the exported repository is developed in krcd002.py and krcd003.py.
The SPaDE native repository format is described in SPaDENativeRepo.md.