Binding Logic: Proofs and Models

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.

Authors

• Gilles Dowek
• Thérèse Hardin
• Claude Kirchner

Keywords

No keywords are indexed for this paper.