RiuNet UPV Home
:
Browsing by Subject

Search RiuNet

Browse

All of RiuNet

My Account

RiuNet Help

Admin. UPV

Browsing by Subject "Operational termination"

Now showing items 1-8 of 8

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 ...
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 ...
Normal forms and normal theories in conditional rewriting

Lucas Alba, Salvador; Meseguer, Jose (Elsevier, 2016-01)

We present several new concepts and results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs), which support types, subtypes and rewriting modulo axioms, and contains the ...
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 ...
Use of logical models for proving infeasibility in term rewriting

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

[EN] Given a (Conditional) Rewrite System R and terms s and t, we consider the following problem: is there a substitution a instantiating the variables in s and t such that the reachability test sigma(s) -> *(R) sigma(t) ...
Use of Logical Models for Proving Operational Termination in General Logics

Lucas Alba, Salvador (Springer Verlag (Germany), 2016-08)

[EN] A declarative programming language is based on some logic L and its operational semantics is given by a proof calculus which is often presented in a natural deduction style by means of inference rules. Declarative ...
Using Well-Founded Relations for Proving Operational Termination

Lucas Alba, Salvador (Springer-Verlag, 2020-02)

[EN] In this paper, we study operational termination, a proof theoretical notion for capturing the termination behavior of computational systems. We prove that operational termination can be characterized at different ...