The language theory of Automath : Chapter VIII, 1 and 2 (AUT-II)

D.T. van Daalen

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureHoofdstukAcademic


    There are two languages of the Automath family that have been developed for practical (in contrast with, say, language theoretical) purposes and have actually been applied in extensive formalization projects. On the one hand there is AUT-QE, used by L.S. van Benthem Jutting in his Landau translation [van Benthem Jutting ‘77]. The latter reference also contains an informal introduction to the language [van Daalen 73 (A.3)]. The theory of AUT-QE is to be found in [van Daalen 80, Ch. IV to VI] [large parts of which are included in this Volume]. On the other hand there is AUT-il, invented by J. Zucker, and employed by Zucker and A. Kornaat for the formalization of classical analysis and some related topics. In [Zucker 77 (A.4)] one finds a short account of both the language and the formalization project. This chapter is devoted to the theory of AUT-il, which is not quite as complete as the theory of AUT-QE. Some work remains to be done, notably on the extensional version of the language (see [C.5, VIII.6]).
    Originele taal-2Engels
    TitelSelected Papers on Automath
    RedacteurenR.P. Nederpelt, J.H. Geuvers, R.C. Vrijer, de
    Plaats van productieAmsterdam
    UitgeverijNorth-Holland Publishing Company
    ISBN van geprinte versie0-444-89822-0
    StatusGepubliceerd - 1994

    Publicatie series

    NaamStudies in Logic


    Duik in de onderzoeksthema's van 'The language theory of Automath : Chapter VIII, 1 and 2 (AUT-II)'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit