This directory contains the design and implementation of the Knowledge Repository component of the SPaDE project.
The files in this directory are organized as follows:
This section includes documents that provide the philosophical context and rationale for the design of the Knowledge Repository. This supplements the general philosophical materials in the docs directory.
At the moment we have two muddled documents in this section, which will be rationalised in due course.
This section includes documents that outline the architectural design of the Knowledge Repository.
This section includes documents that provide a high-level design of the Knowledge Repository.
This section includes documents that provide a detailed design of the Knowledge Repository.
This section includes documents that provide detailed formal specifications or code for the Knowledge Repository.
krcd002.py - Python translation of kr/krdd001.md HOL datatypes
This section includes documents that describe the testing and evaluation process for the Knowledge Repository.
The following is the previous content of this file. It is being retained temporarily for reference while the new structure is being populated. This material will either be moved into the new structure or into other documents in this directory or deleted.
The Knowledge Repository is a core component of the SPaDE architecture that provides a distributed, shared repository for declarative knowledge. It breaks with the traditional LCF paradigm by decoupling knowledge storage from the deductive kernel, permitting the repository to be distributed and open ended.
The Knowledge Repository is structured around the concept of contexts which are similar to theories in other HOL ITP systems, but which are not repositories for theorems (which are held in caches managed by di specialists in each context). The term theory is used to refer to a collection of context extensions (usually conservative) which yields a new context by introducing new names and constraints.
Metatheory is intended to be a significant feature of SPaDE, and metatheory will in general relate to specific theories, but the metadata will be held in its own distinct theories. A major part of such metadata is expected to be the demonstration of derived rules of inference, use of which is expected to displace in SPaDE the role of tactics and other high level proof facilities in more tranditional LCF proof support.
See the main project CONTRIBUTING.md for general guidelines.
Software supporting the knowledge repository is not a single monolith, because it is required to provide access from multiple programming languages and environments, to multiple forms of stored information viewed as theories in the repository.
We therefore require an abstract specification of the structure of the repository, and a variety of interfaces which mediate between stored data and software systems interpreting the stored representations as contexts in the repository, and presenting the interpretation in a form suitable for the specific programming environment.
There are therefore many opportunities for collaboration by contributing to the development of these interfaces and specifications.
Some stored forms will have been specifically designed for this repository, but others will be heritage formats that need to be interpreted, a process which involves making explicit the semantics of the data. In these latter cases, the metadata supplying that interpretation may (and ideally should) be held in the knowledge repository as metatheory.