3 papers
cs.LO2024
Automated Strategy Invention for Confluence of Term Rewrite Systems
Liao Zhang, Fabian Mitterwallner, Jan Jakubuv +1
Term rewriting plays a crucial role in software verification and compiler optimization. With dozens of highly parameterizable techniques developed to prove various system propertie…
cs.LO2024
Confluence of Logically Constrained Rewrite Systems Revisited
Jonas Schöpf, Fabian Mitterwallner, Aart Middeldorp
We show that (local) confluence of terminating locally constrained rewrite systems is undecidable, even when the underlying theory is decidable. Several confluence criteria for log…
cs.LO2023
Linear Termination over N is Undecidable
Fabian Mitterwallner, Aart Middeldorp, René Thiemann
Recently it was shown that it is undecidable whether a term rewrite system can be proved terminating by a polynomial interpretation in the natural numbers. In this paper we show th…