Binding Logic: proofs and models
Logic in Computer Science
2023-05-26 v1
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.
Cite
@article{arxiv.2305.15782,
title = {Binding Logic: proofs and models},
author = {Gilles Dowek and Thérèse Hardin and Claude Kirchner},
journal= {arXiv preprint arXiv:2305.15782},
year = {2023}
}
Comments
Colloque avec actes et comit{\'e} de lecture. internationale