home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #1 / NN_1993_1.iso / spool / comp / ai / 4795 < prev    next >
Encoding:
Internet Message Format  |  1993-01-08  |  2.0 KB
  1. Xref: sparky comp.ai:4795 comp.lang.prolog:2342 sci.logic:2552
  2. Newsgroups: comp.ai,comp.lang.prolog,sci.logic
  3. Path: sparky!uunet!cs.utexas.edu!torn!nott!cunews!bond
  4. From: bond@sce.carleton.ca (Greg Bond)
  5. Subject: Decision procedure for Horn theories with inequality
  6. Message-ID: <bond.726521497@regulus.sce.carleton.ca>
  7. Sender: news@cunews.carleton.ca (News Administrator)
  8. Organization: Carleton University
  9. Date: Fri, 8 Jan 1993 19:31:37 GMT
  10. Lines: 41
  11.  
  12. I'm curious whether there exists a refutation complete decision
  13. procedure for Horn clause theories with *inequality*, namely
  14. "not-equals". For example, consider the definite clause program
  15. defining the negation of path and arc relations for the following
  16. directed graph:
  17.  
  18.     A-->B-->D
  19.  
  20. not_path(x,z) :- not_arc(x,z),not_arc(x,k(x,z)).
  21. not_path(x,z) :- not_arc(x,z),not_path(k(x,z),z)).
  22.  
  23. not_arc(X,Y) :- (X != a),(X != b).
  24. not_arc(X,Y) :- (X != a),(Y != d).
  25. not_arc(X,Y) :- (Y != b),(X != b).
  26. not_arc(X,Y) :- (Y != b),(Y != d).
  27.  
  28. This program is simply the Skolem normal form of the ONLY-IF sentences
  29. of the predicate completion of a definite program defining the
  30. (positive) path and arc relations.  The functor k/2 is a Skolem
  31. function introduced through Skolemization. Note that not_path and
  32. not_arc are predicate symbols here. Inequality is represented by !=
  33. which can either be interpreted to be a predicate symbol or as the
  34. logical negation of equality. The standard equality axioms can be
  35. considered implicit as can the following (lexical) inequalities:
  36.  
  37. (a != b).
  38. (a != d).
  39. (b != d).
  40.  
  41. I would like to be able to confirm that a refutation exists for ground
  42. goals like :- not_path(b,a). This can be done using the OTTER theorem
  43. prover and linear paramodulation but it seems to me there must be a
  44. specialized approach for dealing with Horn clause theories. 
  45.  
  46. Please reply via email and I will summarize for the net.
  47. --
  48. Greg Bond   ----->   bond@sce.carleton.ca  (613) 788 2600 (ext.1835)
  49. Dept. of Systems and Computer Engineering, Carleton University
  50. Ottawa, ON, Canada K1S 5B6
  51.