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