Termination of rewrite systems by elementary interpretations

DOI10.1007/BF01214624MaRDI QIDQ1805401zbMATH OpenFDO

Authors Pierre Lescanne

Publication date 11 May 1995

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF01214624

zbMATH Keywords

rewrite systemsterminationtotal connectionwell-foundedness

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Termination of rewriting systems by polynomial interpretations and its implementation
• Termination of term rewriting by interpretation
• Automatic proofs of termination with elementary interpretations
• Termination of term rewriting: Interpretation and type elimination

Cites work

• scientific article; zbMATH DE number 4016226 (Why is no real title available?)
• scientific article; zbMATH DE number 4047066 (Why is no real title available?)
• scientific article; zbMATH DE number 18651 (Why is no real title available?)
• scientific article; zbMATH DE number 50648 (Why is no real title available?)
• Termination by completion
• Termination of rewriting systems by polynomial interpretations and its implementation
• Termination orderings for associative-commutative rewriting systems

Cited in

(12)

• scientific article; zbMATH DE number 1722702 (Why is no real title available?)
• Innermost termination of rewrite systems by labeling
• Preuves de terminaison de systèmes de réécriture fondées sur les interprétations polynomiales. Une méthode basée sur le théorème de Sturm
• Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations
• More problems in rewriting
• Automatic proofs of termination with elementary interpretations
• Computer Science Logic
• Termination of rewriting systems by polynomial interpretations and its implementation
• Termination of term rewriting by interpretation
• A survey of ordinal interpretations of type ɛ0 for termination of rewriting systems
• Termination proofs for ground rewrite systems -- interpretations and derivational complexity
• Mechanically proving termination using polynomial interpretations

Describes a project that uses

Uses Software

• LARCH
• ORME
• REVE

This page was built for publication: Termination of rewrite systems by elementary interpretations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1805401)