34 citations · 144 across the 66 of their papers we have counts for
43 papers · 1 filter
Nominal semantics for predicate logic: algebras, substitution, quantifiers, and limits
Gilles Dowek, Murdoch J. Gabbay
We define a model of predicate logic in which every term and predicate, open or closed, has an absolute denotation independently of a valuation of the variables. For each variable…
Permissive-Nominal Logic (journal version)
Gilles Dowek, Murdoch J. Gabbay
Permissive-Nominal Logic (PNL) is an extension of first-order predicate logic in which term-formers can bind names in their arguments. This allows for direct axiomatisations with b…
Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques
Gilles Dowek, Murdoch J. Gabbay, Dominic Mulligan
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…
Cut elimination for Zermelo set theory
Gilles Dowek, Alexandre Miquel
We show how to express intuitionistic Zermelo set theory in deduction modulo (i.e. by replacing its axioms by rewrite rules) in such a way that the corresponding notion of proof en…
Relative normalization
Gilles Dowek, Alexandre Miquel
G{ö}del's second incompleteness theorem forbids to prove, in a given theory U, the consistency of many theories-in particular, of the theory U itself-as well as it forbids to prove…
Embedding Pure Type Systems in the lambda-Pi-calculus modulo
Denis Cousineau, Gilles Dowek
The lambda-Pi-calculus allows to express proofs of minimal predicate logic. It can be extended, in a very simple way, by adding computation rules. This leads to the lambda-Pi-calcu…
Arithmetic as a theory modulo
Gilles Dowek, Benjamin Werner
We present constructive arithmetic in Deduction modulo with rewrite rules only.
On Statman's Finite Completeness Theorem
Richard Statman, Gilles Dowek
We give a complete self-contained proof of Statman's finite completeness theorem and of a corollary of this theorem stating that the -definability conjecture implies the higher-…
On the Definition of the Eta-long Normal Form in Type Systems of the Cube
Gilles Dowek, Gérard Huet, Benjamin Werner
The smallest transitive relation < on well-typed normal terms such that if t is a strict subterm of u then t < u and if T is the normal form of the type of t and the term t is not…
The Undecidability of Typability in the Lambda-Pi-Calculus
Gilles Dowek
The set of pure terms which are typable in the -calculus in a given context is not recursive. So there is no general type inference algorithm for the programming language Elf…
The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable
Gilles Dowek
We prove that the pattern matching problem is undecidable in polymorphic lambda-calculi (as Girard's system F) and calculi supporting inductive types (as G{ö}del's system T) by red…
A Complete Proof Synthesis Method for the Cube of Type Systems
Gilles Dowek
We present a complete proof synthesis method for the eight type systems of Barendregt's cube extended with -conversion. Because these systems verify the proofs-as-objects paradi…
Third Order Matching is Decidable
Gilles Dowek
The higher order matching problem is the problem of determining whether a term is an instance of another in the simply typed -calculus, i.e. to solve the equation a = b where a…
Time arrow without past hypothesis: a toy model explanation
Pablo Arrighi, Gilles Dowek, Amélia Durbec
The laws of Physics are time-reversible, making no qualitative distinction between the past and the future -- yet we can only go towards the future. This apparent contradiction is…
Automated theorem proving in first-order logic modulo: on the difference between type theory and set theory
Gilles Dowek
Resolution modulo is a first-order theorem proving method that can be applied both to first-order presentations of simple type theory (also called higher-order logic) and to set th…
Axioms vs. rewrite rules: from completeness to cut elimination
Gilles Dowek
Combining a standard proof search method, such as resolution or tableaux, and rewriting is a powerful way to cut off search space in automated theorem proving, but proving the comp…
From proof theory to theories theory
Gilles Dowek
In the last decades, several objects such as grammars, economical agents, laws of physics... have been defined as algorithms. In particular, after Brouwer, Heyting, and Kolomogorov…
The Stratified Foundations as a theory modulo
Gilles Dowek
The Stratified Foundations are a restriction of naive set theory where the comprehension scheme is restricted to stratifiable propositions. It is known that this theory is consiste…
Binding Logic: proofs and models
Gilles Dowek, Thérèse Hardin, Claude Kirchner
We define an extension of predicate logic, called Binding Logic, where variables can be bound in terms and in propositions. We introduce a notion of model for this logic and prove…
What is a Theory ?
Gilles Dowek
Deduction modulo is a way to express a theory using computation rules instead of axioms. We present in this paper an extension of deduction modulo, called Polarized deduction modul…
Preliminary investigations on induction over real numbers
Gilles Dowek
The induction principle for natural numbers expresses that when a property holds for some natural number a and is hereditary, then it holds for all numbers greater than or equal to…
Confluence as a cut elimination property
Gilles Dowek
The goal of this note is to compare two notions, one coming from the theory of rewrite systems and the other from proof theory: confluence and cut elimination. We show that to each…
A constructive proof of Skolem theorem for constructive logic
Gilles Dowek, Benjamin Werner
If the sequent (Gamma entails forall x exists y A) is provable in first order constructive natural deduction, then the theory (Gamma, forall x (f (x)/y)A), where f is a new functio…
What do we know when we know that a theory is consistent?
Gilles Dowek
Given a first-order theory and a proof that it is consistent, can we design a proof-search method for this theory that fails in finite time when it attempts to prove the formula Fa…