infChecker: A Tool for Checking Infeasibility





Publicado en

Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019)


CC BY 4.0


Given a CTRS R and terms s and t, we say that the reachability condition s = t is feasible if there is a substitution sigma instantiating the variables in s and t such that the reachability test sigma(s) ->*R sigma(t) succeeds; otherwise, we call it infeasible. Given a sequence of reachability conditions (s1 = t1),...,(sn = tn), where n > 0, we say that the sequence is R-feasible if there is a substitution such that all the reachability tests sigma(si) ->*R sigma(ti) are satised. In [5, 6] we presented an approach to deal with infeasibility using a semantic criterion. In this paper we present infChecker, a new tool for checking infeasibility conditions of CTRSs based on this approach. We succesfully participated in the 2019 Confuence Competition in the INF (infeasibility) category, being the most powerful tool for checking both infeasibility and feasibility.


Acerca de Gutiérrez, Raúl

Palabras clave

Conditional Term Rewriting, First-Order Logic, Infeasibility
Página completa del ítem
Notificar un error en este artículo
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX