06/12/2001: Gilles Dowek (INRIA Roquencourt)
Un théorème de complétude pour une extension de la logique du premier ordre avec des symboles lieurs (ou mutificateurs).

We define an extension of first-order logic where variables can be bound in terms and in propositions. We define a notion of model for this logic and we prove a completeness theorem. This theorem is proved as a consequence of the first-order completeness theorem, by encoding this logic back into first-order logic.