Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martı́-Oliet, José Meseguer, Rubén Rubio, Carolyn Talcott · Lecture notes in computer science · 2022
Abstract Equational unification and matching are fundamental mechanisms in many automated deduction applications. Supporting them efficiently for as wide as possible a class of equational theories, and in a typed manner supporting type hierarchies, benefits many applications; but this is both challenging and nontrivial. We present Maude 3.2’s efficient support of these features as well as of symbolic reachability analysis of infinite-state concurrent systems based on them.