DISQUS

chimezie · 2 years ago

I'd be curious to see how a tableau proof compares to a resolution-based proof. "AI: A Modern Approach" has a nice unification heuristic [1] (in python as well) for a backward chaining algorithm which is similar to how prolog unifies and the basis for Deroo's euler-enhanced resolution mechanism for proof and backward chaining.

I've recently pondered hooking up the python RETE-UL [2] implementation I've been playing with a means to track a non-circular path through the RETE network as an alternative proof generation mechanism for large rulesets and factbases. I wonder if there is some metric for comparing the application of LP heuristics to DLP reasoning against (more traditional) resolution and tableux-based heuristics for the same KR.

Generated proofs, whether or not they are truely valuable, bring about a certain unmatchable satisfaction to a logician =)

[1] http://aima.cs.berkeley.edu/python/logic.html
[2] http://reports-archive.adm.cs.cmu.edu/anon/1995...

Bijan Parsia · 2 years ago

I'll be using a ground semantic calculus, since that's what's most commonly used in DL reasoners. I suppose I could do a free variable one as well, which will pop in unification.

RETE and LP (by which I presume you mean logic programming) don't most naturally conflate in my lexicon. The bog standard framework for LP is resolution, from Prolog and Datalog to disjunctive datalog and answer set programming.

But the most natural metric would be performance, I would think :)

And do you mean "optimizations" by "heuristics"? Many optimizations are not heuristic, at least not in how I understand "heuristic".