AlphaProof's Greatest Hits

In a sense, yes, since it has a foundation in Prolog style facts and rules, and supposedly can output its reasoning.

Ok, sounds like in principle you could have proofs, but in practice, you don't?

Are there any checks for the consistency of all facts?

How could there be? Gödel gets in the way.

In most interactive theorem provers the check is simple: you single out the axioms you believe, and all other stuff you do is guaranteed to preserve consistency. That works in an ITP system because there are only a few axioms.

If Cyc has 100000 axioms/facts, then that's a problem.

If axioms, facts and rules have types, these types can guide choice.

It's not a theorem prover, it's more like a support system for decision making.

They can probably isolate 100k facts from some domain for you if you pay for it, but their idea is to run inference on millions of "common sense" and everyday facts and have been for decades.

That sounds to me like something that will be subsumed by the combination of ITP and AI.

Not a believer in types here, sorry. I'd rather have simple theorems instead without wading through a swamp of types first. And I am sure AI will be able to handle theorems just fine.

They've refused to die for many, many years by now. Not sure what you mean by ITP but if it's thrombocytopenia, they claim to have a lot of customers in medicine already.