Calculating Church-Rosser proofs in Kleene algebra

DOI10.1007/3-540-36280-0_19MaRDI QIDQ4415087zbMATH OpenFDO

Authors Georg Struth

Publication date 28 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2561/25610276.htm

zbMATH Keywords

\(\lambda\)-calculusChurch-Rosser theoremformal mathematicsKleene algebrarewriting

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Grammars and rewriting systems (68Q42) Algebraic theory of languages and automata (68Q70)

Recommendations

• Abstract abstract reduction
• Church–Rosser Made Easy
• More Church-Rosser proofs (in Isabelle/HOL)
• More Church-Rosser proofs (in Isabelle/HOL)
• A mechanical proof of the Church-Rosser theorem

Cited in

(7)

• The Church Rosser theorem for strong reduction in combinatory logic
• Abstract strategies and coherence
• Automated Reasoning for Hybrid Systems — Two Case Studies —
• More Church-Rosser proofs (in Isabelle/HOL)
• Algebraic coherent confluence and higher globular Kleene algebras
• Diagonalisation and Church's Thesis: Kleene's Homework
• Abstract abstract reduction

This page was built for publication: Calculating Church-Rosser proofs in Kleene algebra

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