Una plataforma para el uso combinado de procesadores en la demostración de la terminación de la reescritura

Abstract

[ES] Realizar una herramienta que demuestra la terminación de sistemas de reescritura utilizando el denominado Marco de Pares de Dependencia (\emph{DP Framework}) a partir de procesadores aportados por usuarios externos. Dichos procesadores son evaluados antes de utilizarse para garantizar cierto grado de seguridad. La herramienta acepta sistemas de reescritura de términos en formato TPDB (Termination Problem Data Base) y permite la definición de una estrategia de terminación a partir de los procesadores disponibles. La demostración se realiza siguiendo la estrategia introducida y se presenta al usuario de forma uniforme a partir de los reportes parciales obtenidos de la ejecución de cada procesador. Dicha demostración incluye la procedencia de cada procesador utilizado.

[EN] Developing a tool which can be used to prove the termination of term rewriting systems using the Dependency Pair Framework (\emph{DP Framwork}) based on processors supplied by external users. These processors are evaluated before they are available in order to guarantee certain degree of security. This tool accepts term rewriting systems in TPDB (Termination Problem Data Base) format and it allows users the definition of a termination strategy by combining the available processors. The demonstration is built following the strategy entered, and it is uniformly shown to the user by collecting the partial reports generated by each processor. The demonstration also includes the origin of each processor used.