- From: Tanel Tammet <tammet@staff.ttu.ee>
- Date: Thu, 03 Apr 2003 20:25:00 +0300
- To: joachim.peer@unisg.ch
- Cc: www-rdf-logic@w3.org
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
Received on Thursday, 3 April 2003 12:24:33 UTC