Skip to Main content Skip to Navigation
Conference papers

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
Document type :
Conference papers
Complete list of metadatas
https://hal.inria.fr/inria-00101012
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 2:53:30 PM
Last modification on : Tuesday, April 21, 2020 - 1:11:20 AM

Identifiers

  • HAL Id : inria-00101012, version 1

Collections

INRIA | CNRS | X | UPMC | LIP6 | UMR8623 | LORIA | UNIV-LORRAINE | SORBONNE-UNIVERSITE | SU-SCIENCES

Citation

Gilles Dowek, Thérèse Hardin, Claude Kirchner. Binding Logic: proofs and models. 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR'2002, Oct 2002, Tbilisi, Georgia. pp.130-144. ⟨inria-00101012⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

271

 

Contact                    Legal Notice                    Personal Data