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-11 of 11

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 ...
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 ...
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, 09-2018)

[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 ...