DocumentCode
2294398
Title
Notational definition-a formal account
Author
Griffin, Timothy G.
Author_Institution
Cornell Univ., Ithaca, NY, USA
fYear
1988
fDate
0-0 1988
Firstpage
372
Lastpage
383
Abstract
In the course of developing a mathematical theory or proof it is a common practice to introduce new notation to represent notation that is previously understood. The author presents a formal account that is intended to model the practice of introducing and using notational (abbreviate) definitions. The aim of this work is a pragmatic one: to provide a framework useful in the design and implementation of secure proof system interfaces which accommodate, as much as possible, conventional mathematical practice. A typed lambda -calculus is used to represent expressions of a given object language. A Delta -equation is introduced to model conventional definition equations.<>
Keywords
formal logic; Delta -equation; Nupol system; abbreviate definitions; definition equations; mathematical theory; new notation; notational definitions; object language; proof; secure proof system interfaces; typed lambda -calculus; Calculus; Equations; Logic; Mathematics;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1988. LICS '88., Proceedings of the Third Annual Symposium on
Conference_Location
Edinburgh, UK
Print_ISBN
0-8186-0853-6
Type
conf
DOI
10.1109/LICS.1988.5134
Filename
5134
Link To Document