RT Conference Proceedings
T1 Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
A1 Durán, Francisco
A1 Eker, Steven
A1 Escobar, Santiago
A1 Martí Oliet, Narciso
A1 Meseguer, José
A1 Rubio Cuéllar, Rubén Rafael
A1 Talcott, Carolyn
A2 Blanchette, Jasmin
A2 Kovács, Laura
A2 Pattinson, Dirk
AB 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.
SN 9783031107689
SN 9783031107696
SN 0302-9743
SN 1611-3349
YR 2022
FD 2022
LK https://hdl.handle.net/20.500.14352/94853
UL https://hdl.handle.net/20.500.14352/94853
LA eng
NO Agencia Estatal de Investigación
NO Junta de Andalucía
NO FEDER
NO European Union
NO Generalitat Valenciana
NO U. S. Office of Naval Research
DS Docta Complutense
RD 19 abr 2025