scientific article
From MaRDI portal
Publication:2985126
DOI10.23638/LMCS-13(2:4)2017zbMath1398.68485arXiv1612.07195MaRDI QIDQ2985126
Julian Nagele, Bertram Felgenhauer, Harald Zankl
Publication date: 16 May 2017
Full work available at URL: https://arxiv.org/abs/1612.07195
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Uses Software
Cites Work
- Decreasing diagrams and relative termination
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem
- Confluence by decreasing diagrams
- More Church-Rosser proofs (in Isabelle/HOL)
- Isabelle/HOL. A proof assistant for higher-order logic
- Formal proofs about rewriting using ACL2
- Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
- Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
- Confluence by Decreasing Diagrams – Formalized
- Certification of Termination Proofs Using CeTA
- Confluence Competition 2015
- Confluence by Decreasing Diagrams
- Code Generation via Higher-Order Rewrite Systems
- Proving Confluence of Term Rewriting Systems Automatically
- A mechanical proof of the Church-Rosser theorem
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Term Rewriting and All That
- CSI – A Confluence Tool
- Certified Rule Labeling
- Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative
- Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling.
- Tree-Manipulating Systems and Church-Rosser Theorems
- Parallel reductions in \(\lambda\)-calculus
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication:
