Author name cluster

Raúl Gutiérrez

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

2 author rows

LOPSTR Conference 2022 Conference Paper

Confluence Framework: Proving Confluence with CONFident

Raúl Gutiérrez
Miguel Vítores
Salvador Lucas

Abstract This paper describes CONFident, a tool which is able to automatically prove and disprove confluence of variants of rewrite systems: term rewriting systems, conditional term rewriting systems (using join, oriented, or semi-equational semantics), and context-sensitive term rewriting systems. We introduce a new proof framework to generate proof trees by combining different techniques for proving confluence (including modular decompositions, checking joinability of (conditional) critical pairs, transformations, etc.). We also use external tools for proving termination and operational termination ( mu-term ), or feasibility ( infChecker ) and deducibility ( Prover9 ).

Details

LOPSTR Conference 2017 Conference Paper

Variant-Based Decidable Satisfiability in Initial Algebras with Predicates

Raúl Gutiérrez
José Meseguer 0001

Abstract 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 quantifier-free satisfiability in the initial algebra of an order-sorted equational theory \((\varSigma, E \cup B)\) under two conditions: (i) \(E \cup B\) has the finite variant property and B has a finitary unification algorithm; and (ii) \((\varSigma, E \cup B)\) protects a constructor subtheory \((\varOmega, E_{\varOmega } \cup B_{\varOmega })\) that is OS- compact. These conditions apply to many user-definable theories, but have a main limitation: they apply well to data structures, but often do not hold for user-definable predicates on such data structures. We present a theory-generic satisfiability decision procedure, and a prototype implementation, extending variant-based satisfiability to initial algebras with user-definable predicates under fairly general conditions.

Details

LOPSTR Conference 2014 Conference Paper

Extending the 2D Dependency Pair Framework for Conditional Term Rewriting Systems

Salvador Lucas
José Meseguer 0001
Raúl Gutiérrez

Abstract Recently, a new dependency pair framework for proving operational termination of Conditional Term Rewriting Systems (CTRSs) has been introduced. We call it 2D Dependency Pair (DP) Framework for CTRSs because it makes explicit and exploits the bidimensional nature of the termination behavior of conditional rewriting, where rewriting steps \(s\rightarrow t\) and rewritings \(s\rightarrow ^*t\) (in zero or more steps) are defined for specific terms \(s\) and \(t\) by using an inference system where appropriate proof trees should be exhibited for such particular goals. In this setting, the horizontal component of the termination behavior concerns the existence of infinite sequences of rewriting steps, and the vertical component captures infinitely many climbs during the development of a proof tree for a single rewriting step. In this paper we extend the 2D DP Framework for CTRSs with several powerful processors for proving and disproving operational termination that specifically exploit the structure of conditional rules. We provide the first implementation of the 2D DP Framework as part of the termination tool mu-term. Our benchmarks suggest that, with our new processors, the 2D DP Framework is currently the most powerful technique for proving operational termination of CTRSs.

Details

LOPSTR Conference 2013 Conference Paper

A Transformational Approach to Resource Analysis with Typed-Norms

Elvira Albert
Samir Genaim
Raúl Gutiérrez

Abstract In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along a program’s execution. Typically, analyzers measure the sizes of data by applying norms which are mappings from data to natural numbers that represent the sizes of the corresponding data. When norms are defined by taking type information into account, they are named typed-norms. The main contribution of this paper is a transformational approach to resource analysis with typed-norms. The analysis is based on a transformation of the program into an intermediate abstract program in which each variable is abstracted with respect to all considered norms which are valid for its type. We also sketch a simple analysis that can be used to automatically infer the required, useful, typed-norms from programs.

Details

I&C Journal 2010 Journal Article

Context-sensitive dependency pairs

Beatriz Alarcón
Raúl Gutiérrez
Salvador Lucas

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 proposed so far, the adaptation to CSR of the dependency pair approach, one of the most powerful techniques for proving termination of rewriting, took some time and was possible only after introducing some new notions like collapsing dependency pairs, which are specific for CSR. In this paper, we develop the notion of context-sensitive dependency pair (CSDP) and show how to use CSDPs in proofs of termination of CSR. The implementation and practical use of the developed techniques yield a novel and powerful framework which improves the current state-of-the-art of methods for automatically proving termination of CSR.

Details DOI

LPAR Conference 2008 Conference Paper

Improving Context-Sensitive Dependency Pairs

Beatriz Alarcón
Fabian Emmes
Carsten Fuhs
Jürgen Giesl
Raúl Gutiérrez
Salvador Lucas
Peter Schneider-Kamp
René Thiemann

Abstract Context-sensitive dependency pairs (CS-DPs) are currently the most powerful method for automated termination analysis of context-sensitive rewriting. However, compared to DPs for ordinary rewriting, CS-DPs suffer from two main drawbacks: (a) CS-DPs can be collapsing. This complicates the handling of CS-DPs and makes them less powerful in practice. (b) There does not exist a “ DP framework ” for CS-DPs which would allow one to apply them in a flexible and modular way. This paper solves drawback (a) by introducing a new definition of CS-DPs. With our definition, CS-DPs are always non-collapsing and thus, they can be handled like ordinary DPs. This allows us to solve drawback (b) as well, i. e. , we extend the existing DP framework for ordinary DPs to context-sensitive rewriting. We implemented our results in the tool AProVE and successfully evaluated them on a large collection of examples.

Details