Canonical Narrowing for Variant-Based Conditional Rewrite Theories

Abstract

23rd International Conference on Formal Engineering Methods (ICFEM 2022). Madrid, Spain: Springer. Maude currently supports many symbolic reasoning features such as order-sorted equational unification and order-sorted narrowingbased symbolic reachability analysis. There have been many advances and new features added to improve narrowing in Maude but only at a theoretical level. In this paper, we provide a very elegant, transparent, and extremely pragmatic approach for conditional rewrite theories where the conditions are just equalities solved by equational unification. We show how two conditional theories, never executed before, are now executable with very good performance.We also show how real execution works better than the manually transformed version.