Comment by ants_everywhere
3 days ago
I don't know why you're getting downvoted because I think this is an interesting idea.
Completely impossible but still interesting and fun to explore.
But you don't need the power of Lean to do something like this. I would recommend starting with something like Prolog or RDF triples
Basically [Citation Needed]
[flagged]
Argument mining and automatic fact checking are things and there are actual products that do them.
It seems reasonable to have some of those products implemented in a logic language.
I think a logic language is not a great fit, because it deals in absolute truths. Whereas news and non-fiction articles are more someone said something and they are usually reliable except in this particular domain where they can be a bit biased sometimes. Also the people they interviewed may have misremembered. Etc etc.
You could argue that all such things could in principle be modelled in logical formulas but... it would be way more complicated than the stated model.
On the other hand it's also unclear what the logical model actually adds. Usually logical formulas are used because they can be manipulated, and inferences can be drawn. But drawing logical inferences from sorta-kinda true statements can quickly become muddy and lead to false conclusions if you don't take into account the uncertainty of the statements.
4 replies →
But such system exists, mostly implemented in prolog.
Does it actually?
4 replies →