RiuNet UPV Home
:
Browsing by Author

Search RiuNet

Browse

All of RiuNet

My Account

RiuNet Help

Admin. UPV

Browsing by Author "Meseguer, José"

Now showing items 1-13 of 13

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é (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. ...
A Modular Order-sorted Equational Generalization Algorithm

Alpuente Frasnedo, María; Escobar Román, Santiago; Espert Real, Javier; Meseguer, José (Elsevier, 2014-04)

Generalization, also called anti-unification, is the dual of unification. Given terms t and t , a generalizer is a term t of which t and t are substitution instances. The dual of a most general unifier (mgu) is that of ...
A Partial Evaluation Framework for Order-sorted Equational Programs modulo Axioms

Alpuente Frasnedo, María; Cuenca-Ortega, Angel Eduardo; Escobar Román, Santiago; Meseguer, José (Elsevier, 2020-01)

[EN] Partial evaluation is a powerful and general program optimization technique with many successful applications. Existing PE schemes do not apply to expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ...
ACUOS: A System for Modular ACU Generalization with Subtyping and Inheritance

Alpuente Frasnedo, María; Escobar Román, Santiago; Espert Real, Javier; Meseguer, José (Springer, 2014)

Computing generalizers is relevant in a wide spectrum of automated reasoning areas where analogical reasoning and inductive inference are needed. The ACUOS system computes a complete and minimal set of semantic generalizers ...
ACUOS: A System for Modular ACU Generalization with Subtyping and Inheritance (extended version)

Alpuente, María; Escobar, Santiago; Espert, Javier; Meseguer, José (2014-07-16)

Computing generalizers is relevant in a wide spectrum of automated reasoning areas where analogical reasoning and inductive inference are needed. The ACUOS system computes a complete and minimal set of semantic generalizers ...
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 ...
Models for logics and conditional constraints in automated proofs of termination

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

Reasoning about termination of declarative programs, which are described by means of a computational logic, requires the definition of appropriate abstractions as semantic models of the logic, and also handling the conditional ...
Protocol analysis modulo combination of theories: A case study in Maude-NPA

Sasse, Ralf; Escobar Román, Santiago; Meadows, Catherine; Meseguer, José (Springer Verlag (Germany), 2011)

There is a growing interest in formal methods and tools to analyze cryptographic protocols modulo algebraic properties of their underlying cryptographic functions. It is well-known that an intruder who uses algebraic ...
Proving Operational Termination of Declarative Programs in General Logics

Lucas Alba, Salvador; Meseguer, José (ACM, 2014-09)

A declarative program P is a *theory* in a given computational logic L, so that *computation* with such a program is efficiently implemented as *deduction* in L. That is why *inference systems* are crucial: they both (i) ...
Strong and weak operational termination of order-sorted rewrite theories

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

This paper presents several new results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs) which contains the more restricted framework of conditional term rewriting systems ...
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 ...
Variant-Based Decidable Satisfiability in Initial Algebras with Predicates

Gutiérrez Gil, Raúl; Meseguer, José (Springer-Verlag, 2018)

[EN] Decision procedures can be either theory-specific, e.g., Presburger arithmetic, or theory-generic, applying to an infinite number of user-definable theories. Variant satisfiability is a theory-generic procedure for ...