RT Report
T1 Strategies in Conditional Narrowing Modulo SMT Plus Axioms
T2 Estrategias en Estrechamiento Condicional Módulo SMT más Axiomas
A1 Aguirre Garcia, Luis Manuel
A1 Martí Oliet, Narciso
A1 Palomino, Miguel
A1 Pita Andreu, Isabel
AB Narrowing calculus that uses strategies to solve reachability problems in order-sorted rewrite theories whose underlying equational logic is composed of SMT theories plus some combination of associativity, commutativity, and identity. Both the strategies and the rewrite rules are allowed to be parameterized, i.e., they may have a set of common constants that are given a value as part of the solution of a problem. The soundness and weak completeness of the calculus are proved.
YR 2021
FD 2021-11-05
LK https://hdl.handle.net/20.500.14352/5848
UL https://hdl.handle.net/20.500.14352/5848
LA eng
NO Ministerio de Ciencia e Innovación (MICINN)
NO Comunidad de Madrid/FEDER
DS Docta Complutense
RD 7 may 2024