Proof-theoretic techniques for term rewriting theory.

Nachum Dershowitz, Mitsuhiro Okada

Research output: Chapter in Book/Report/Conference proceedingConference contribution

32 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationProc Third Annu Symp on Logic in Comput Sci
PublisherPubl by IEEE
Pages104-111
Number of pages8
ISBN (Print)0818608536
Publication statusPublished - 1988
Externally publishedYes

Fingerprint

Religious buildings
Computer science

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Dershowitz, N., & Okada, M. (1988). Proof-theoretic techniques for term rewriting theory. In Proc Third Annu Symp on Logic in Comput Sci (pp. 104-111). Publ by IEEE.

Proof-theoretic techniques for term rewriting theory. / Dershowitz, Nachum; Okada, Mitsuhiro.

Proc Third Annu Symp on Logic in Comput Sci. Publ by IEEE, 1988. p. 104-111.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Dershowitz, N & Okada, M 1988, Proof-theoretic techniques for term rewriting theory. in Proc Third Annu Symp on Logic in Comput Sci. Publ by IEEE, pp. 104-111.
Dershowitz N, Okada M. Proof-theoretic techniques for term rewriting theory. In Proc Third Annu Symp on Logic in Comput Sci. Publ by IEEE. 1988. p. 104-111
Dershowitz, Nachum ; Okada, Mitsuhiro. / Proof-theoretic techniques for term rewriting theory. Proc Third Annu Symp on Logic in Comput Sci. Publ by IEEE, 1988. pp. 104-111
@inproceedings{28fe4c2c34be46e891f495d173a80d02,
title = "Proof-theoretic techniques for term rewriting theory.",
abstract = "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",
year = "1988",
language = "English",
isbn = "0818608536",
pages = "104--111",
booktitle = "Proc Third Annu Symp on Logic in Comput Sci",
publisher = "Publ by IEEE",

}

TY - GEN

T1 - Proof-theoretic techniques for term rewriting theory.

AU - Dershowitz, Nachum

AU - Okada, Mitsuhiro

PY - 1988

Y1 - 1988

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0024132219&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0024132219&partnerID=8YFLogxK

M3 - Conference contribution

SN - 0818608536

SP - 104

EP - 111

BT - Proc Third Annu Symp on Logic in Comput Sci

PB - Publ by IEEE

ER -