home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #16 / NN_1992_16.iso / spool / comp / theory / 1672 < prev    next >
Encoding:
Internet Message Format  |  1992-07-21  |  1.2 KB
  1. Path: sparky!uunet!mcsun!corton!sophia!almeria.inria.fr!bob
  2. From: bob@almeria.inria.fr (Renaud Marlet)
  3. Newsgroups: comp.theory
  4. Subject: Recent survey on decidability results for equational theories & TRS
  5. Message-ID: <24870@sophia.inria.fr>
  6. Date: 21 Jul 92 13:44:16 GMT
  7. Sender: news@sophia.inria.fr
  8. Organization: INRIA, Sophia-Antipolis (Fr)
  9. Lines: 26
  10.  
  11.  
  12. Could somebody suggest a reference to a recent survey on decidability
  13. results for equational theories and TRS. Thanks.
  14.  
  15. -- Renaud  [bob@sophia.inria.fr]
  16.  
  17.  
  18. -----------------------------------------------------------------------------
  19. PS: just in case somebody knows... Given the axioms for /\,\/,T,F such that:
  20.  
  21. Associativity    (x /\ y) /\ z = x /\ (y /\ z)
  22.         (x \/ y) \/ z = x \/ (y \/ z)
  23. Distributivity    x /\ (y \/ z) = (x /\ y) \/ (x /\ z)
  24.         x \/ (y /\ z) = (x \/ y) /\ (x \/ z)
  25. Left identity    T /\ x = x
  26.         F \/ x = x
  27. Left zero    F /\ x = F
  28.         T \/ x = T
  29.  
  30. Plus a bunch of ground axioms on other function symbols. For example:
  31.  
  32.         f(g(a,b),c) \/ k(l) = h(d) /\ (e \/ i(j))
  33.  
  34. What good (confluent, noetherian) a TRS may be found for these axioms?  Same
  35. question with the addition of the commutativity of /\ and \/. Many thanks.
  36. -----------------------------------------------------------------------------
  37.