%0 Conference Paper
%A Durán, Francisco 
%A Eker, Steven 
%A Escobar, Santiago 
%A Martí Oliet, Narciso
%A Meseguer, José 
%A Rubio Cuéllar, Rubén Rafael
%A Talcott, Carolyn 
%T Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
%D 2022
%@ 0302-9743
%@ 1611-3349
%U https://hdl.handle.net/20.500.14352/94853
%X 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.
%~