Abstract
Notational definitions are pervasive in mathematical practice and are therefore supported in most automated theorem proving systems such as Coq [B+98], PVS [ORS92], Lego [LP92], or Isabelle [Pau94]. Semantically, notational definitions are transparent, that is, one obtains the meaning of an expression by interpreting the result of expanding all definitions. Pragmatically, however, expanding all definitions as they are encountered is unsatisfactory, since it can be computationally expensive and complicate the user interface.
This work was supported by NSF Grant CCR-9619584
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bruno Barras et al. The Coq Proof Assistant, Reference Manual, Version 6.2. INRIA, CNRS, France, 1998. 179
Iliano Cervesato and Frank Pfenning. A linear spine calculus. Technical Report CMU-CS-97-125, CMU, 1997. 180, 181
Gilles Dowek, Thérése Hardin, Claude Kirchner, and Frank Pfenning. Unification via explicit substitutions: The case of higher-order patterns. In Joint International Conference and Symposium on Logic Programming (JICSLP’ 96), Bonn, Germany, 1996. 189
Timothy G. Griffin. Notational definition — a formal account. In Third Annual Symposium on Logic in Computer Science, Edinburgh, Scotland, pages 372–383. IEEE, July 1988. 180
M. Hanus. The integration of functions into logic programming: From theory to practice. Journal of Logic Programming, 19&20:583–628, 1994. 180
Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143–184, January 1993. 179, 180, 181, 182, 183
Chris Hankin and Daniel Le Métayer. Deriving algorithms from type inference systems: Application to strictness analysis. In Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, Portland, pages 202–212. ACM, January 1994. 188
Robert Harper and Frank Pfenning. A module system for a programming language based on the LF logical framework. Journal of Logic and Computation, 8(1):5–31, 1998. A preliminary version is available as Technical Report CMU-CS-92-191, September 1992. 183
Gérard Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975. 180, 184
Zhaohui Luo and Robert Pollack. The LEGO proof development system: A user’s manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, May 1992. 179
Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991. 186
S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752, Saratoga, NY, June 1992. Springer-Verlag. 179
Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer-Verlag LNCS 828, 1994. 179
Frank Pfenning. Unification and anti-unification in the Calculus of Constructions. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 74–85, Amsterdam, The Netherlands, July 1991. 190
Frank Pfenning and Carsten Schürmann. Twelf User’s Guide, 1.2 edition, September 1998. Available as Technical Report CMU-CS-98-173, Carnegie Mellon University. 180, 188
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pfenning, F., Schürmann, C. (1999). Algorithms for Equality and Unification in the Presence of Notational Definitions. In: Altenkirch, T., Reus, B., Naraschewski, W. (eds) Types for Proofs and Programs. TYPES 1998. Lecture Notes in Computer Science, vol 1657. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48167-2_13
Download citation
DOI: https://doi.org/10.1007/3-540-48167-2_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66537-3
Online ISBN: 978-3-540-48167-6
eBook Packages: Springer Book Archive