Binding Logic: proofs and models

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

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…