Buscar en RiuNet

Listar

Todo RiuNet

Mi cuenta

Acceder

Ayuda RiuNet

Admin. UPV

Listar por palabra clave "Dependency pairs"

Mostrando ítems 1-15 de 15

2D Dependency Pairs for Proving Operational Termination of CTRSs

Lucas Alba, Salvador; Meseguer, José (Springer Verlag (Germany), 2014-11)

The notion of *operational termination* captures nonterminating computations due to subsidiary processes that are necessary to issue a *single* `main' step but which often remain `hidden' when the main computation sequence ...
A Dependency Pair Framework for AvC-Termination

Alarcón Jiménez, Beatriz; Gutiérrez Gil, Raúl; Lucas, Salvador; Meseguer, José (Universitat Politècnica de València, 2011-05-04)

The development of powerful techniques for proving termination of rewriting modulo a set of equational axioms is essential when dealing with rewriting logic-based programming languages like CafeOBJ, Maude, ELAN, OBJ, etc. ...
Context-Sensitive Dependency Pairs

Alarcón, Beatriz; Gutiérrez Gil, Raúl; Lucas Alba, Salvador (Springer-Verlag, 2006)

[EN] Termination is one of the most interesting problems when dealing with context-sensitive rewrite systems. Although there is a good number of techniques for proving termination of context-sensitive rewriting (CSR), the ...
Context-Sensitive Dependency Pairs

Alarcón, Beatriz; Gutiérrez Gil, Raúl; Lucas Alba, Salvador (Elsevier, 2010-08)

[EN] Termination is one of the most interesting problems when dealing with context-sensitive rewrite systems. Although a good number of techniques for proving termination of context-sensitive rewriting (CSR) have been ...
Context-Sensitive Dependency Pairs Framework

Gutiérrez Gil, Raúl (Universitat Politècnica de València, 2011-11-28)

We show how to develop a dependency pair framework for proving termination of context-sensitive rewriting.
Dependency pairs for proving termination properties of conditional term rewriting systems

Lucas Alba, Salvador; Meseguer, José (Elsevier, 2017-01)

[EN] The notion of operational termination provides a logic-based definition of termination of computational systems as the absence of infinite inferences in the computational logic describing the operational semantics of ...
Improving the Context-Sensitive Dependency Graph

Alarcón, Beatriz; Gutiérrez Gil, Raúl; Lucas Alba, Salvador (Elsevier, 2007-07-16)

[EN] The dependency pairs method is one of the most powerful technique for proving termination of rewriting and it is currently central in most automatic termination provers. Recently, it has been adapted to be used in ...
Innermost Termination of Context-Sensitive Rewriting

Alarcón Jiménez, Beatriz; Lucas, Salvador (Universitat Politècnica de València, 2011-05-04)

Innermost context-sensitive rewriting (CSR) has been proved useful for modeling the computational behavior of programs of algebraic languages like Maude, OBJ, etc, which incorporate an innermost strategy which is used to ...
Innermost Termination of Context-Sensitive Rewriting

Alarcón Jiménez, Beatriz (Universitat Politècnica de València, 2011-11-28)

Innermost context-sensitive rewriting (CSR) has been proved useful for modeling the computational behavior of programs of algebraic languages like Maude. We adapt the Dependency Pairs Framework to innermost CSR since, up ...
Relative Termination via Dependency Pairs

Iborra, José; Nishida, Naoki; Vidal Oriola, Germán; Yamada, Akihisa (Springer-Verlag, 2017)

[EN] A term rewrite system is terminating when no infinite reduction sequences are possible. Relative termination generalizes termination by permitting infinite reductions as long as some distinguished rules are not applied ...
Termination of Narrowing with Dependency Pairs

Iborra López, José (Universitat Politècnica de València, 2011-11-28)

In this work, we generalize the Dependency Pairs approach for automated proofs of termination to prove the termination of narrowing.We identify the phenomenon of echoing in infinite narrowing derivations and demonstrate ...
The 2D Dependency Pair Framework for conditional rewrite systems. Part I: Definition and basic processors

Lucas Alba, Salvador; Meseguer, José; Gutiérrez Gil, Raúl (Elsevier, 2018-09)

[EN] Different termination properties of conditional term rewriting systems have been recently described emphasizing the bidimensional nature of the termination behavior of conditional rewriting. The absence of infinite ...
The 2D Dependency Pair Framework for Conditional Rewrite Systems¿Part II: Advanced Processors and Implementation Techniques

Lucas Alba, Salvador; Meseguer, José; Gutiérrez Gil, Raúl (Springer-Verlag, 2020-10)

[EN] Proving termination of programs in `real-life¿ rewriting-based languages like CafeOBJ, Haskell, Maude, etc., is an important subject of research. To advance this goal, faithfully cap- turing the impact in the termination ...
Una plataforma para el uso combinado de procesadores en la demostración de la terminación de la reescritura

Martínez López, Alejandro (Universitat Politècnica de València, 2022-10-21)

[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. ...
Usable Rules for Context-Sensitive Rewrite Systems

Gutiérrez Gil, Raúl; Lucas Alba, Salvador; Urbain, Xavier (Springer-Verlag, 2008)

[EN] Recently, the dependency pairs (DP) approach has been generalized to context-sensitive rewriting (CSR). Although the context-sensitive dependency pairs (CS-DP) approach provides a very good basis for proving termination ...