1.  50
    Proof Normalization Modulo.Gilles Dowek & Benjamin Werner - 2003 - Journal of Symbolic Logic 68 (4):1289-1316.
    We define a generic notion of cut that applies to many first-order theories. We prove a generic cut elimination theorem showing that the cut elimination property holds for all theories having a so-called pre-model. As a corollary, we retrieve cut elimination for several axiomatic theories, including Church's simple type theory.
    Direct download (10 more)  
    Export citation  
    Bookmark   5 citations  
  2.  37
    A Simple Proof That Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
    We give a simple and direct proof that super-consistency implies the cut-elimination property in deduction modulo. This proof can be seen as a simplification of the proof that super-consistency implies proof normalization. It also takes ideas from the semantic proofs of cut elimination that proceed by proving the completeness of the cut-free calculus. As an application, we compare our work with the cut-elimination theorems in higher-order logic that involve V-complexes.
    Direct download (7 more)  
    Export citation  
    Bookmark   1 citation  
  3.  5
    Third Order Matching is Decidable.Gilles Dowek - 1994 - Annals of Pure and Applied Logic 69 (2-3):135-155.
    The higher order matching problem is the problem of determining whether a term is an instance of another in the simply typed [lgr]-calculus, i.e. to solve the equation a = b where a and b are simply typed [lgr]-terms and b is ground. The decidability of this problem is still open. We prove the decidability of the particular case in which the variables occuring in the problem are at most third order.
    Direct download (4 more)  
    Export citation  
    Bookmark   2 citations  
  4.  4
    Permissive Nominal Terms and Their Unification: An Infinite, Co-Infinite Approach to Nominal Techniques (Vol 8, Pg 769, 2010). [REVIEW]Gilles Dowek, Murdoch J. Gabbay & Dominic Mulligan - 2012 - Logic Journal of the IGPL 20 (1):769-822.
    Nominal terms extend first-order terms with binding. They lack some properties of first- and higher-order terms: Terms must be reasoned about in a context of ‘freshness assumptions’; it is not always possible to ‘choose a fresh variable symbol’ for a nominal term; it is not always possible to ‘α-convert a bound variable symbol’ or to ‘quotient by α-equivalence’; the notion of unifier is not based just on substitution. Permissive nominal terms closely resemble nominal terms but they recover these properties, and (...)
    No categories
    Direct download (3 more)  
    Export citation  
    Bookmark   1 citation  
  5.  4
    Axioms Vs. Rewrite Rules: From Completeness to Cut Elimination.Gilles Dowek - 2000 - In Dov M. Gabbay & Maarten de Rijke (eds.), Frontiers of Combining Systems. Research Studies Press. pp. 62--72.
  6.  1
    Les Origines de L'Informatique.Gilles Dowek - 2015 - Cahiers Philosophiques 2:7.
    No categories
    Direct download (2 more)  
    Export citation  
  7. Ouro Preto (Minas Gerais), Brazil July 29–August 1, 2003.France Xii, Marcelo Coniglio, Gilles Dowek, Jouko Väänanen, Renata Wassermann, Eric Allender, Jean-Baptiste Joinet & Dale Miller - 2004 - Bulletin of Symbolic Logic 10 (2).