4 ms·
Does Cyc have proofs?
by auggierose 2y ago
Does Cyc have proofs?
- cess11 2y agoIn a sense, yes, since it has a foundation in Prolog style facts and rules, and supposedly can output its reasoning.
- auggierose 2y agoOk, sounds like in principle you could have proofs, but in practice, you don't? Are there any checks for the consistency of all facts?
- cess11 2y agoHow could there be? Gödel gets in the way.
- auggierose 2y agoIn 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.
- thesz 2y agoIf axioms, facts and rules have types, these types can guide choice.
- auggierose 2y agoNot 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.
- cess11 2y agoIt'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.
- auggierose 2y agoThat sounds to me like something that will be subsumed by the combination of ITP and AI.
- cess11 2y agoThey'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.