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.
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 : Thursday, March 21, 2019 - 2:16:43 PM

Identifiers

  • HAL Id : inria-00101012, version 1

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⟩

Share

Metrics

Record views

242