TruSpark is built on formal standards and ontologies that other people wrote, maintain, and give away. This page names them.
A platform that asks you to check its reasoning should be equally clear about whose reasoning it inherited. Everything below is the work of communities that published it for others to build on, and TruSpark would not exist without any of it.
The top-level ontology every layer of a TruSpark theory is grounded in. BFO is developed and maintained by the BFO community, originated by Barry Smith and colleagues, and standardised as the second part of ISO/IEC 21838. Its 2020 revision is the version TruSpark implements. basic-formal-ontology.org
The logic in which every TruSpark theory is written. The Common Logic Interchange Format is defined by ISO/IEC 24707, developed through ISO/IEC JTC 1/SC 32.
An open repository of carefully axiomatised Common Logic theories covering mereology, time, process and space, contributed by independent research groups and assembled at the Semantic Technologies Laboratory, University of Toronto, under Michael Grüninger. TruSpark's parser is tested against COLORE, and the coverage figure quoted elsewhere on this site is measured against that corpus. The number is only meaningful because the corpus exists. github.com/gruninger/colore
A community of ontology developers maintaining interoperable ontologies for the life sciences under shared principles. TruSpark recognises OBO conventions when reading a corpus, and draws on Foundry ontologies including the Information Artifact Ontology (IAO) and the Relation Ontology (RO). obofoundry.org
A suite of mid-level ontologies extending BFO, providing terms that recur across domains rather than within any one of them. github.com/CommonCoreOntology
A community effort building BFO-grounded ontologies for manufacturing and industrial domains. TruSpark recognises IOF conventions when reading a corpus on its own terms. industrialontologies.org
TruSpark's prover portfolio runs alongside OntoProver, our own prover built for BFO 2020. Z3 is developed at Microsoft Research; CVC5 by the cvc5 team across Stanford, the University of Iowa and collaborating institutions; Vampire at the University of Manchester and collaborators. A verdict this platform reports as proved may have been decided by any of them, and the certificate says which.
If your work is used here and is credited wrongly, incompletely, or not at all, we would rather hear it than not. Please tell us and we will correct this page.