Related papers: Rewriting modulo in Deduction modulo
We present a new modular proof method of termination for second-order computation, and report its implementation SOL. The proof method is useful for proving termination of higher-order foundational calculi. To establish the method, we use a…
There are many evaluation strategies for term rewrite systems, but automatically proving termination or analyzing complexity is usually easiest for innermost rewriting. Several syntactic criteria exist when innermost termination implies…
We propose a modular method for proving termination of general logic programs (i.e., logic programs with negation). It is based on the notion of acceptable programs, but it allows us to prove termination in a truly modular way. We consider…
The notion of computability closure has been introduced for proving the termination of higher-order rewriting with first-order matching by Jean-Pierre Jouannaud and Mitsuhiro Okada in a 1997 draft which later served as a basis for the…
In a previous work, the first author extended to higher-order rewriting and dependent types the use of size annotations in types, a termination proof technique called type or size based termination and initially developed for ML-like…
All current investigations to analyze the derivational complexity of term rewrite systems are based on a single termination method, possibly preceded by transformations. However, the exclusive use of direct criteria is problematic due to…
We explore the Collatz conjecture and its variants through the lens of termination of string rewriting. We construct a rewriting system that simulates the iterated application of the Collatz function on strings corresponding to mixed…
Convergent rewriting systems on algebraic structures give methods to solve decision problems, to prove coherence results, and to compute homological invariants. These methods are based on higher-dimensional extensions of the critical…
In this paper we examine a number of term rewriting system for integer number representations, building further upon the datatype defining systems described in [2]. In particular, we look at automated methods for proving confluence and…
Term rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving…
A rewriting system is a set of equations over a given set of terms called rules that characterize a system of computation and is a powerful general method for providing decision procedures of equational theories, based upon the principle of…
We study the termination problem for probabilistic term rewrite systems. We prove that the interpretation method is sound and complete for a strengthening of positive almost sure termination, when abstract reduction systems and term rewrite…
We obtain, for the first time, a modular many-valued semantics for combined logics, which is built directly from many-valued semantics for the logics being combined, by means of suitable universal operations over partial non-deterministic…
The lambda Pi calculus can be extended with rewrite rules to embed any functional pure type system. In this paper, we show that the embedding is conservative by proving a relative form of normalization, thus justifying the use of the lambda…
The rewriting system sigma is the set of rules propagating explicit substitutions in the lambda-calculus with explicit substitutions. In this note, we prove the undecidability of unification modulo sigma.
We define a notion of model for the $\lambda$$\Pi$-calculus modulo theory and prove a soundness theorem. We then define a notion of super-consistency and prove that proof reduction terminates in the $\lambda$$\Pi$-calculus modulo any…
We investigate the computability of algebraic closure and definable closure with respect to a collection of formulas. We show that for a computable collection of formulas of quantifier rank at most $n$, in any given computable structure,…
We present techniques to prove termination of cycle rewriting, that is, string rewriting on cycles, which are strings in which the start and end are connected. Our main technique is to transform cycle rewriting into string rewriting and…
The term {\em meta-programming} refers to the ability of writing programs that have other programs as data and exploit their semantics. The aim of this paper is presenting a methodology allowing us to perform a correct termination analysis…
The lambda-Pi-calculus Modulo is a variant of the lambda-calculus with dependent types where beta-conversion is extended with user-defined rewrite rules. It is an expressive logical framework and has been used to encode logics and type…