"The axioms are acquired from the Web and translated into a kind of logic program. The proof engine uses the resolution inference mechanism and only follows Euler paths (the concept Euler found several hundred years ago) so that endless deductions are avoided. That means that no special attention has to be paid to recursions or to graph merging."
C# and Java versions available! Having N3 in Jena 1.6 is obviously going to help this. He also is using OWL.
The actual source code is very procedural, converting it with the visitor pattern, plug in a standard RDF parser and triple store, add some visualization software and it would be very neat.