2019/10/21 by António Malheiro, Paulo Guilherme Santos, Malheiro, António +1
Computer Science · #68Q42 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1910.09254
openalex publication_date 2019/10/21 · openalex created_date 2019/10/25 · openalex updated_date 2026/07/28
In this note we give a simple unifying proof of the undecidability of several diagrammatic properties of term rewriting systems that include: local confluence, strong confluence, diamond property, subcommutative property, and the existence of successor. The idea is to code configurations of Turing Machines into terms, and then define a suitable relation on those terms such that the termination of the Turing Machine becomes equivalent to the satisfiability of the diagrammatic property.