The SPaDE project has the following main objectives:
To argue that the abstract representation of the logic known as Cambridge HOL is suitable as a general representation form for declarative knowledge irrespective of what language or coding it may have been presented or stored in.
To articulate a conception of a deductive paradigm shift which, with the benefit of effective automation only possible through AI will transform the exploitation of declarative knowledge from computation processes of uncertain effect to formally verified computation yielding unambiguous and reliable truths.
To specify APIs and protocols for access to a distrbuted shared repository of knowledge. The abstract form of knowledge is that of the abstract syntax of HOL and the abstract semantics is also that of HOL. The concrete forms may be diverse, and concrete semantics addresses the material world by giving concrete interpretation for various abstract domains. Arbitrary sources of data can be viewed as incorporated into this scheme, wither by treating it as data (i.e. assigning explicit values to new names), or by semantic embeddings, shallow or deep.
To build an abstract inference engine supporting those processes in a manner independent of the concrete syntax or stored form of the knowledge which forms the logical context for the inference.