IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Third Annual IEEE Symposium on

Logic in Computer Science (LICS 1988)

Paper: Proof-theoretic techniques for term rewriting theory (at LICS 1988)

Authors: Nachum Dershowitz Mitsuhiro Okada


A bridge is presented between term-rewriting theory in computer science and proof theory in logic. It is shown that proof-theoretic tools are very useful for analyzing two basic attributes of term rewriting systems, the termination property and the Church-Rosser property. A counterexample is given to show that Knuth's critical pair lemma does not hold for conditional rewrite systems. Two restrictions on conditional systems under which the critical pair lemma holds are presented. One is considered a generalization of Bergstra-Klop's former result; the other is concerned with a generalization of Kaplan's and Jouannaud-Waldmann's systems


    author = 	 {Nachum Dershowitz and Mitsuhiro Okada},
    title = 	 {Proof-theoretic techniques for term rewriting theory},
    booktitle =  {Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988)},
    year =	 {1988},
    month =	 {July}, 
    pages =      {104--111},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}

Last modified: 2017-04-0512:37
Andrzej Murawski