The Undecidability of Unification Modulo $\sigma$ Alone
Logic in Computer Science
2023-05-11 v1
Abstract
The rewriting system sigma is the set of rules propagating explicit substitutions in the lambda-calculus with explicit substitutions. In this note, we prove the undecidability of unification modulo sigma.
Keywords
Cite
@article{arxiv.2305.06214,
title = {The Undecidability of Unification Modulo $\sigma$ Alone},
author = {Gilles Dowek},
journal= {arXiv preprint arXiv:2305.06214},
year = {2023}
}