logical equivalence of horn clauses?

(sorry for re-posting -  my first email was cut off for some reason..)

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)"

I need such an algorithm for a prototyp i am currently planning, a semantic 
web service matchmaking engine. The Horn Clauses would serve as Pre- and 
Postconditions assigned to service operations.

I have the feeling there MUST be some algorithm (or some proof why such an 
algorithm does NOT exist), but i don't know where I should start to look.

thanks for any hints !!

joachim

-- 
Joachim Peer, 
Research Assistant, 
MCM institute, University of St. Gallen,
Blumenbergplatz 9, 9000 St. Gallen, Switzerland
Phone: 0041-71-224-3441, Fax: 0041-71-224-2771
joachim.peer@unisg.ch http://sws.mcm.unisg.ch/jpeer

Received on Thursday, 3 April 2003 10:39:39 UTC