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.


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