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

D.T. van Daalen

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademic


    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]).
    Original languageEnglish
    Title of host publicationSelected Papers on Automath
    EditorsR.P. Nederpelt, J.H. Geuvers, R.C. Vrijer, de
    Place of PublicationAmsterdam
    PublisherNorth-Holland Publishing Company
    ISBN (Print)0-444-89822-0
    Publication statusPublished - 1994

    Publication series

    NameStudies in Logic


    Dive into the research topics of 'The language theory of Automath : Chapter VIII, 1 and 2 (AUT-II)'. Together they form a unique fingerprint.

    Cite this