The Knowledge Repository
This directory covers the architecture, design and implementation of the Knowledge Repository component of the SPaDE project.
The files in this directory are organized as follows:
- Philosophical Background (krph) - Foundational philosophical ideas influencing the design of the knowledge repository.
- Architectural Design (krad) - High-level architecture and design of the knowledge repository.
- High Level Design (krhd) - Detailed high-level design considerations for the knowledge repository.
- Detailed Design (krdd) - Low-level design and implementation details.
- Code (krcd)- Detailed formal specifications and code.
- Testing and Evaluation (krte) - Prototyping strategies and implementations for the knowledge repository.
- Task Descriptions (krtd) - Task descriptions for implementing knowledge repository components.
- Build Configuration (krci) - Makefiles and build configuration.
Philosophical Background
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 three muddled documents in this section, which will be rationalised in due course.
Architectural Design
This section includes documents that outline the architectural design of the Knowledge Repository.
- krad001.md - Knowledge Repository Architecture Overview
High Level Design
This section includes documents that provide a high-level design of the Knowledge Repository.
- krhd002.md - Prototyping strategies for knowledge repository development
- krhd003.md - Scraping ProofPower HOL Theories into a SPaDE Repository
Detailed Design
This section includes documents that provide a detailed design of the Knowledge Repository.
Code
This section includes documents that provide detailed formal specifications or code for the Knowledge Repository.
- krcd001.sml - Signature describing the encoding/I/O/S-expression contracts for SPaDE Native Repository I/O
- krcd006.sml - HOL4 specification of SPaDE repository
- krcd008.py - Abstract Base Classes for SPaDE Native Repository I/O (following krdd004.md)
- krcd009.py - Concrete Python implementation of SPaDE Native Repository I/O (implements krcd008)
- krcd010.sml - SML signatures detailing the Native Repository encoding/I/O/S-expression contracts
- krcd011.sml - SML structures implementing the Native Repository encoding/I/O/S-expression contracts
- krcd012.py - Python wrapper that delegates the Native Repository I/O ABCs to the SML implementation in krcd011.sml via a persistent ProofPower session
- krcd013.py - Python interface to an interactive theorem prover (e.g., ProofPower) (coded by Gemini 3 Pro)
Testing and Evaluation
This section includes documents that describe the testing and evaluation process for the Knowledge Repository.
- krte001.md - Knowledge repository prototyping test notes
- krte002.py - Integration tests for krcd009.py (SPaDE Native Repository I/O)
- krte003.py - Unit tests for krcd009.py (SPaDE Native Repository I/O)
- krte004.sml - SML unit smoke tests for krcd011 Native Repository implementation
- krte005.py - Integration tests for krcd011 Native Repository implementation
- krte006.sml - Extended SML tests covering krcd011 Native Repository I/O and S-expressions
Task Descriptions
This section includes task descriptions for implementing knowledge repository components.
- krtd001.md - Task Description for Python ABC for SPaDE Native Repository I/O
- krtd002.md - Task Description for Code ad Test Low Level Native Repository I/O in SML.
- krtd003.md - Task Description for SML Signatures for SPaDE Native Repository I/O
Build Configuration
This section includes makefiles and build configuration.