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

Browse the full CPP paper archive.