65 citations · 93 across the 10 of their papers we have counts for
10 papers
Drag Rewriting
Nachum Dershowitz, Jean-Pierre Jouannaud, Fernando Orejas
We present a new and powerful algebraic framework for graph rewriting, based on drags, a class of graphs enjoying a novel composition operator. Graphs are embellished with roots an…
Confluence of Layered Rewrite Systems
Jean-Pierre Jouannaud, Jiaxiang Liu, Mizuhito Ogawa
We investigate the new, Turing-complete class of layered systems, whose lefthand sides of rules can only be overlapped at a multiset of disjoint or equal positions. Layered systems…
The computability path ordering
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability pa…
The computability path ordering: the end of a quest
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we p…
From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
We investigate here a new version of the Calculus of Inductive Constructions (CIC) on which the proof assistant Coq is based: the Calculus of Congruent Inductive Constructions, whi…
HORPO with Computability Closure : A Reconstruction
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
This paper provides a new, decidable definition of the higher- order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for…