2012/10/01 by Harald Zankl, Zankl, Harald
Computer Science · #Advanced Database Systems and Queries #F.3.1 #F.4.2 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO
paper · pdf · doi:10.48550/arxiv.1210.1100
17 pages; valley and conversion version; RTA 2013
openalex publication_date 2012/10/01 · arxiv created 2013/04/11 · arxiv updated 2013/04/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
This paper presents a formalization of decreasing diagrams in the theorem prover Isabelle. It discusses mechanical proofs showing that any locally decreasing abstract rewrite system is confluent. The valley and the conversion version of decreasing diagrams are considered.