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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi, L. Cardelli, P.-L. Curien, J.-J. Lévy, Explicit substitutions, Journal of Functional Programming, 1,4 (1991) pp. 375–416.
P.B. Andrews, An introduction to mathematical logic and type theory: to truth through proof, Academic Press (1986).
A. Barber, Dual Intuitionistic Linear Logic, Technical Report ECS-LFCS-96-347, University of Edinburgh (1996).
N.G. de Bruijn, Lambda calculus notation with nameless dummies: a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indag. Math. 34, pp 381–392.
P.-L. Curien, Categorical combinators, sequential algorithms and functional programming, Birkhauser (1993).
P.-L. Curien, Th. Hardin and J.-J. Lévy, Weak and strong confluent calculi of explicit substitutions, Journal of the ACM, 43,2 (1996) pp. 362–397.
H.B. Curry, R. Feys, Combinatory Logic, I, North Holland, Amsterdam (1958).
G. Dowek, La part du calcul, Mémoire d’Habilitation à Diriger des Recherches, Université de Paris VII (1999).
G. Dowek, Th. Hardin and C. Kirchner, Higher-order unification via explicit substitutions, Information and Computation, 157 (2000) pp. 183–235.
G. Dowek, Th. Hardin and C. Kirchner, Theorem proving modulo, Rapport de Recherche 3400, INRIA (1998). To appear in Journal of Automated Reasonning.
G. Dowek, Th. Hardin and C. Kirchner, HOL-lambda-sigma: an intensional first-order expression of higher-order logic, Mathematical Structures in Computer Science, 11 (2001) pp. 1–25.
G. Dowek and B. Werner, Proof normalization modulo, Types for Proofs and Programs 98, T. Altenkirch, W. Naraschewski, B. Rues (Eds.), Lecture Notes in Computer Science 1657, Springer-Verlag (1999), pp. 62–77.
M. Fiore, G. Plotkin, and D. Turi, Abstract syntax and variable binding, Logic in Computer Science (1999) pp. 193–202.
L. Henkin, Completeness in the theory of types, The Journal of Symbolic Logic, 15 (1950) pp. 81–91.
J.R. Hindley, Combinatory reductions and lambda reductions compared, Zeit. Math. Logik, 23 (1977) pp. 169–180.
J. Lambek, Deductive systems and categories II. Standard constructions and closed categories. Category theory, homology theory and their applications I, Lecture Notes in Mathematics, 86, Springer-Verlag (1969) pp. 76–122.
J. Lambek, Multicategories revisited, Contemporary Mathematics, 92 (1989) 217–239.
D. Miller and G. Nadathur, A logic programming approach to manipulating formulas and programs. Symposium on Logic Programming (1987).
B. Pagano, X.R.S: eXplicit Reduction Systems, a first-order calculus for higher-order calculi, Conference on Automated Deduction, C. Kirchner and H. Kirchner (Eds.), LNAI 1421, Springer-Verlag (1998), pp. 72–88.
B. Pagano, Des calculs de substitution explicites et de leur application a la compilation des langages fonctionnels. Thése de Doctorat, Université de Paris VI (1998).
F. Pfenning and C. Elliott, Higher-order abstract syntax, Conference on Programming Language Design and Implementation, ACM Press, (1988) pp. 199–208.
S. Vaillant, Expressing set theory in first-order predicate logic, International Workshop on Explicit Substitutions Theory and Applications to Programs and Proofs (2000).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dowek, G., Hardin, T., Kirchner, C. (2002). Binding Logic: Proofs and Models. In: Baaz, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2002. Lecture Notes in Computer Science(), vol 2514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36078-6_9
Download citation
DOI: https://doi.org/10.1007/3-540-36078-6_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00010-5
Online ISBN: 978-3-540-36078-0
eBook Packages: Springer Book Archive