Re: please keep Equality in the rule conclusion

On Thu, Feb 25, 2010 at 11:09 AM, Chris Welty <cawelty@gmail.com> wrote:

>
> Actually, I think performance is not the issue, just whether and how hard
> it is to be implemented at all.
>
>
If one wants a complete implementation, I am afraid there is
no way to avoid implementing some form of paramodulation [1],
most likely some ordered version of it. IMO, it is significantly
harder than, say, implementing a RETE, to use a comparison
from the rule engine area.

The good news is that the theory is already very well developed
and there is a significant implementation experience accumulated by the
theorem proving community.


[1] R. Nieuwenhuis and A. Rubio. Paramodulation-Based Theorem Proving.
Handbook of Automated Reasoning,
volume I. 2001.


Cheers,
======================================
Dr. Alexandre Riazanov (Alexander Ryazanov)
Montreal, Canada
cell: +1 - 514 - 961 86 89
http://www.freewebs.com/riazanov/
http://www.linkedin.com/in/riazanov
======================================