## Automatic proofs in the calculus of constructions. (Démonstration automatique dans le calcul des constructions.)(French)Zbl 0849.68111

Rocquencourt: Institut National de Recherche en Informatique et en Automatique (INRIA). 128 p. (Univ. de Paris VII 1991) (1991).
Automated deduction is a challenging subject even for classical (propositional or first-order) logics. The main concern of this thesis is to treat the mentioned theme in higher-order logics (“Dans cette these, nous avons decrit une methode de semi-decision pour les systèmes de types”). “Le calcul des constructions” — as a logical proof-system – is in fact a typed $$\lambda$$-calculus for which the Curry-Howard correspondence is used: “To declare an axiom $$P$$ simple means to declare a variable of type $$P$$ and proving a formula $$P$$ simple means to provide a $$\lambda$$-term of type $$P$$.” The book is divided into three chapters. The first one is mainly introductory (Logique du premier ordre; Logique d’ordre superieur; Systèmes de types; Bonne fondation de la recursion simultanee sur le type et les sous-termes stricts d’un terme). Chapter two (“Demonstration automatique”) is the “core” of this work, its sections being self-explanatory (Contextes quantifies, Constraints, Substitutions: Une méthode complete de synthèse de preuve; Une restriction incomplete). The last chapter is dedicated to the particular case of resolution in equational logics and has three sections (Unification; Equations decidables; Equations indecidables). We think that the thesis contains many valuable original results and conjectures and will be a source of fruitful future research.

### MSC:

 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 03B35 Mechanization of proofs and logical operations 03B40 Combinatory logic and lambda calculus 03B70 Logic in computer science

### Keywords:

automated deduction