The Architecture - rbjones/HoLoTruth GitHub Wiki

The principal elements of the architecture proposed are as follows:

• The Logical Kernel
  There may be more than one logical kernel available to work in the context of the knowledge hierarchy we envisage, often adaptations of existing systems, but we have in mind one brand new kernel with a number of special features which are intended to support the ambitions we have articulated.
• Distributed Theory Hierarchy as Knowledge Base
  Rather than keeping a theory hierarchy private to each instance of a theorem prover, the DA-Hol architecture provides for a single distributed theory hierarchy and a diversity of proof tools, which undertake or contribute to extensions to that hierarchy.
• [Distributed Theory Development] Not only is the hierarchy of contexts and theories distributed, but the process of deriving new theorems may be distributed across the network with different nodes in then network competing to provide the most effective capabilites in different special domains which may contribute to a single result.
• [Assurance Levels] In an elaboration of the scheme whereby "oracles" are admitted subject to tagging of results with information about which oracles they depend upon, proof tools have unique identifiers (URIs) which are combined to give "assurance levels" which tag theorems in a theory, and associated RSA key pairs used to tag and sign theorems
• [Deductive Intelligence] providing Deduction-as-a-Service
• Agents (and people) train and evolve in an [Proof-Market Incubator]