1. A Complete Proof Synthesis Method for the Cube of Type Systems
- Author
-
Gilles Dowek, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)
- Subjects
FOS: Computer and information sciences ,Discrete mathematics ,Computer Science - Logic in Computer Science ,Arts and Humanities (miscellaneous) ,Logic ,Hardware and Architecture ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,Cube (algebra) ,Type (model theory) ,Software ,Logic in Computer Science (cs.LO) ,Theoretical Computer Science ,Mathematics - Abstract
We present a complete proof synthesis method for the eight type systems of Barendregt's cube extended with $\eta$-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.
- Published
- 1993
- Full Text
- View/download PDF