Stardust is top-cover for a small constellation of projects which together take aim at cosmic AI with a deductive core, of which the three main components are:

A project aiming at broad spectrum distributed application of automated and semi-automated deduction in Higher Order Logic.

Concerned with empirical knowledge. how it relates to sense data, and how it mediates in real world effects through activators.

Concerning the formulation and implementation of value systems.


This is a place for me to explore the application of Deep Learning to theorem proving, and various other related matters. Hardly begun, since at the time I started it my ideas were moving pretty fast and I came up with the DA-Hol idea. It remains as a place for me to experiment.


This is a fork of RobArthan’s pp-contrib for me to add contributions to ProofPower. I started to rebuild one of my set theories here (as “ti”) but didn’t get very far. I also set out more recently to put in an interface as Standard ML structures to various Deep Learning packages. This connects with DA-Hol (and XI) but this bit might as well be a contrib to ProofPower.

This is a git repo containing the build system for the web site, which contains most of the output from my intellectual wanderings over the period from about 1994 to 2016.

I am now in the process of mothballing this site as I transition to working only in github hosted development projects. Once this is complete, the site will be purely of historical interest. I might also transfer the web site itself onto if I decide it should still be up.