Confluence of orthogonal term rewriting systems in the prototype verification system
From MaRDI portal
Publication:2362205
DOI10.1007/s10817-016-9376-2zbMath1407.68441OpenAlexW2414463669MaRDI QIDQ2362205
André Luiz Galdino, Mauricio Ayala-Rincón, Ana Cristina Rocha-Oliveira
Publication date: 6 July 2017
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-016-9376-2
critical pairsorthogonalityconfluenceterm rewriting systemnon-terminationleft-linearitynon-ambiguity
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem
- Developing developments
- Checking overlaps of nominal rewriting rules
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- First-order unification in the PVS proof assistant
- Term Rewriting and All That
- Confluence of orthogonal nominal rewriting systems revisited
- Formalizing Bounded Increase
- Tree-Manipulating Systems and Church-Rosser Theorems
- Parallel reductions in \(\lambda\)-calculus
This page was built for publication: Confluence of orthogonal term rewriting systems in the prototype verification system
