arXiv subjects
Publications and source records attributed to 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-order matching conjecture.
We give an algorithm for the class of second order unification problems in which second order variables have at most one occurrence.
System I is a proof language for a fragment of propositional logic where isomorphic propositions, such as $A\wedge B$ and $B\wedge A$, or $A\Rightarrow(B\wedge C)$ and $(A\Rightarrow B)\wedge(A\Rightarrow C)$ are made equal. System I enjoys the strong normalization property. This is sufficient to prove the existence of empty types, but not to prove the introduction property (every closed term in normal form is an introduction). Moreover, a severe restriction had to be made on the types of the variables in order to obtain the existence of empty types. We show here that adding $η$-expansion rules to System I permits to drop this restriction, and yields a strongly normalizing calculus which enjoys the full introduction property.
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 a sort then T < t is well-founded in the type systems of the cube. Thus every term admits a eta-long normal form.
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 and, in some cases, some type information has to be mentioned by the programmer.
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 paradigm, the proof synthesis method is a one level process merging unification and resolution. Then we present a variant of this method, which is incomplete but much more efficient. At last we show how to turn this algorithm into a unification algorithm.
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 reducing Hilbert's tenth problem to it. More generally pattern matching is undecidable in all the calculi in which primitive recursive functions can be fairly represented in a precised sense.
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 and b are simply typed $λ$-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 occurring in the problem are at most third order.
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, mathematical proofs have been defined as algorithms. In this paper, we show that mathematical theories can be also be defined as algorithms and that this definition has some advantages over the usual definition of theories as sets of axioms.
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 completeness of such combined methods may be challenging. It may require in particular to prove cut elimination for an extended notion of proof that combines deductions and computations. This suggests new interactions between automated theorem proving and proof theory.
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 theory. When it is applied to some first-order presentations of type theory, it simulates exactly higherorder resolution. In this note, we compare how it behaves on type theory and on set theory.
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 consistent and that proofs strongly normalize in this theory. Deduction modulo is a formulation of first-order logic with a general notion of cut. It is known that proofs normalize in a theory modulo if it has some kind of many-valued model called a pre-model. We show in this paper that the Stratified Foundations can be presented in deduction modulo and that the method used in the original normalization proof can be adapted to construct a pre-model for this theory.
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 modulo, where some rules can only be used at positive occurrences, while others can only be used at negative ones. We show that all theories in propositional calculus can be expressed in this framework and that cuts can always be eliminated with such theories.
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 a soundness and completeness theorem for it. This theorem is obtained by encoding this logic back into predicate logic and using the classical soundness and completeness theorem there.
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 a. We present a similar principle for real numbers.
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 rewrite system on terms, we can associate a logical system: asymmetric deduction modulo this rewrite system and that the confluence property of the rewrite system is equivalent to the cut elimination property of the associated logical system. This equivalence, however, does not extend to rewrite systems directly rewriting atomic propositions.
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 False?
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 function symbol, is a conservative extension of Gamma.