UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
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.
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⟩
