A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems

Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer
10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021),   pp. 250 – 263, 2021.

abstract   BibTeX   PDF   doi:10.1145/3437992.3439918