Binding Logic: proofs and models

Gilles Dowek 1 Thérèse Hardin 2 Claude Kirchner 3
1 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
2 SPI - Sémantiques, preuves et implantation
LIP6 - Laboratoire d'Informatique de Paris 6
3 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Mots-clés : lieur compléture logique des prédicats binder predicate logic binding logic completeness logique de lieurs
Type de document :
Communication dans un congrès
M. Baaz, A. Voronkov. 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR'2002, Oct 2002, Tbilisi, Georgia. Springer, 2514, pp.130-144, 2002, Lecture notes in Artificial Intelligence
Liste complète des métadonnées
https://hal.inria.fr/inria-00101012
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:53:30
Dernière modification le : vendredi 31 août 2018 - 09:25:58

Identifiants

  • HAL Id : inria-00101012, version 1

Collections

INRIA | X | PARISTECH | UPMC | LIP6 | UMR8623 | LORIA | UNIV-LORRAINE

Citation

Gilles Dowek, Thérèse Hardin, Claude Kirchner. Binding Logic: proofs and models. M. Baaz, A. Voronkov. 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR'2002, Oct 2002, Tbilisi, Georgia. Springer, 2514, pp.130-144, 2002, Lecture notes in Artificial Intelligence. 〈inria-00101012〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

198

Contact


archive-ouverte@inria.fr