help needed: logical equivalence of horn clauses?

Hi all,


could you please take a look at the following problem:

assume we have a horn program (set of horn clauses) and we want to
determine IF 2 of these clauses are "logically equivalent". Let's assume
that there are NO outer-logic extensions (cut, arithmetic evaluation etc.)

An example:

goal1(x,y) <- foo(x,y), helper(x).
helper(x) <- bar(x).
goal2(x,y) <- foo(x,y), bar(y).

Is there an alogrithm to find out wether 2 goals (e.g. "goal1" and "goal2")
are logically equivalent ?  In the example above, the two rules look
equivalent (especially after substituting  helper/1 by bar/1), but they
aren't, since "bar" uses the varibale "x" in one case and "y"  in the other
case. The two clauses would be "logically equivalent", if goal2 would be
defined as "goal2(x,y) <- foo(x,y), bar(x)"

==> My question : is anybody aware of an algorithm to solve this problem? I
want to avoid writing a (probably bad) heuristic only because i am
ignorant, while there might be a good solution out there.

As said before, the horn-like rules carry no outer logic extensions, and
lot's of other assumptions/simplifications can be made (maybe i can even
forbid recursive clauses to make it simpler).

Btw, why do i need such an algorithm - it would be part of a prototype for
web service matchmaking... the horn rules would be used to express pre- and
post-conditions...


many thanks in advance!
joachim


Joachim Peer
Research Assistant
MCM Institute, University of St. Gallen
Blumenbergplatz 9, 9000 St. Gallen, Switzerland
Phone: ++41 (0) 71 224 3441, Fax: ++41 (0) 71 224 2771

Received on Thursday, 3 April 2003 02:53:48 UTC