Tim@UPENN.CSNET (Tim Finin) (02/25/86)
From: Tim Finin <Tim%upenn.csnet@CSNET-RELAY.ARPA>
Forwarded From: Dale Miller <Dale@UPenn> on Mon 24 Feb 1986 at 17:08
UPenn Math-CS Logic Seminar
A Refutation Method for Horn Clauses with Equality using E-unification
Jean H. Gallier (with Stan Raatz)
Tuesday, 25 February 1986, 4:30 - 6:00, 4E17 DRL
A refutation method for equational Horn clauses, Horn clauses with or
without equational atoms, is investigated. This method combines standard
SLD-resolution and unification modulo equations. In the case of ground Horn
clauses, unsatisfiability of a set of Horn clauses with equality is
decidable in time O(nlog(n)). In the general case however, even though the
refutation method itself is complete, unification modulo equations is
undecidable. In fact, unification modulo equations is NP-complete even in
the case of ground equations. Considering this point, we explore subcases
of equational Horn clauses for which unification modulo equations is
tractable, and consider the implications for logic programming. Finally, we
compare this new method with other existing methods.
** Next week: G. Rosolini from CMU will speak on "Categories for Partial
Computations".