Durán, FranciscoEker, StevenEscobar, SantiagoMartí Oliet, NarcisoMeseguer, JoséRubio Cuéllar, Rubén RafaelTalcott, CarolynBlanchette, JasminKovács, LauraPattinson, Dirk2024-01-232024-01-232022978303110768997830311076960302-97431611-334910.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 paperopen accessSymbolic reachabilityRewriting logicNarrowingInteligencia artificial (Informática)Lenguajes de programación1203.04 Inteligencia Artificial1102.14 Lógica Simbólica1203.23 Lenguajes de Programación