RE: logical equivalence of horn clauses?

I used JTP (java theorem prover) quite good and easy to integrate in java
applications.
http://www.ksl.stanford.edu/software/JTP/

Regards,

Charlie

-------------------------------------------------
Charlie Abela
Research Student,
CSAI Dept.,
University of Malta,
MSD06. Malta
Web: http://alphatech.mainpage.net
Email: abcharl@keyworld.net

-----Original Message-----
From: www-rdf-logic-request@w3.org [mailto:www-rdf-logic-request@w3.org]On
Behalf Of Tanel Tammet
Sent: 03 April 2003 19:25
To: joachim.peer@unisg.ch
Cc: www-rdf-logic@w3.org
Subject: Re: logical equivalence of horn clauses?


Hi,

Joachim Peer wrote:
 >
 > 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.)
 >
...
 > Is there an alogrithm to find out wether 2 goals (e.g. "goal1" and
"goal2")
 > are logically equivalent ?

If I remember right, then this problem is known to be undecidable.
Of course, this assumes that you do have function symbols in the
rules.

IMHO the best bet for practical checking (should work almost always
in practice, even if not decidable) is to:

- use a first order prover to attempt to prove equivalence
- if the prover runs over a second (or 1/10 of a second), then
   stop it and use a finite model builder to attempt to show that the
   clauses are not equivalent (again, a second should suffice)

Look at http://www.cs.miami.edu/~tptp/CASC/ to find out about
leading provers and model builders.

Regards,
         Tanel Tammet





All email is scanned by Keyworld against known Viruses. This service is offered to all Keyworld subscribers and hosted domains and does not carry any warranty. You are advised to protect your PC with updated antivirus software at all times.

Received on Thursday, 3 April 2003 12:42:00 UTC