SbReve2: A term rewriting laboratory with (AC)-unfailing completion

  • Siva Anantharaman
  • Jieh Hsiang
  • Jalel Mzali
System Descriptions
Part of the Lecture Notes in Computer Science book series (LNCS, volume 355)


Inference Rule Theorem Prove Critical Pair Canonical System Ground Term 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AM-88]
    S. Anantharaman, J. Mzali, Unfaling Completion Modulo a set of Equations, Technical report, LRI, 1989Google Scholar
  2. [BDP-87]
    L. Bachmair, N. Dershowitz, D. Plaisted, Completion without failure, Proc. Coll. on Resolution of Equations in Algebraic Structures, Lakeway, Texas, 1987Google Scholar
  3. [FG-84]
    R. Forgaard, J. Guttag, REVE: A term rewriting system generator with failure-resistant Knuth-Bendix, MIT-LCS technical report, 1984Google Scholar
  4. [HM-88]
    J. Hsiang, J. Mzali, SbReve users guide, Technical report, LRI, 1988Google Scholar
  5. [HR-87]
    J. Hsiang, M. Rusinowitch, On word problems in equational theories, 14th ICALP,Springer-Verlag LNCS Vol 267, pp54–71, 1987Google Scholar
  6. [HRS-87]
    J. Hsiang, M. Rusinowitch, K. Sakai, Complete set of inference rules for the cancellation laws, IJCAI 87, Milan, Italy, 1987Google Scholar
  7. [St-84]
    M.E. Stickel, A case study of theorem proving by the Knuth-Bendix method: Discovering that x3=x implies ring commutativity, 7th CADE, Springer-Verlag, LNCS Vol 170, pp248–258, 1984Google Scholar
  8. [Mz-86]
    J. Mzali, Methodes de filtrage equationnel et de preuve automatique de theoremes, Thesis, Université de Nancy, 1986Google Scholar
  9. [PS-81]
    G. Peterson, M.E. Stickel, Complete sets of reductions for some equational theories, JACM Vol 28, pp 233–264, 1981Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • Siva Anantharaman
    • 1
  • Jieh Hsiang
    • 2
  • Jalel Mzali
    • 2
  1. 1.LIFO, Dépt. Math-Info.Université d'OrléansOrleans Cedex 02France
  2. 2.Université Paris-Sud OrsayOrsay CedexFrance

Personalised recommendations