Durán, FranciscoEker, StevenEscobar, SantiagoMartí Oliet, NarcisoMeseguer, JoséRubio Cuéllar, Rubén RafaelTalcott, CarolynBlanchette, JasminKovács, LauraPattinson, Dirk2024-01-232024-01-232022978-3-031-10768-9978-3-031-10769-60302-974310.1007/978-3-031-10769-6_31https://hdl.handle.net/20.500.14352/94853Equational 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.engAttribution 4.0 Internationalhttp://creativecommons.org/licenses/by/4.0/conference paper1611-3349open accessSymbolic reachabilityRewriting logicNarrowingInteligencia artificial (Informática)Lenguajes de programación1203.04 Inteligencia Artificial1102.14 Lógica Simbólica1203.23 Lenguajes de Programación