The language theory of Automath : Chapter I, Sections 1-5 (Introduction)

D.T. van Daalen

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademic


    This thesis gives an account of the author’s language theoretical studies on the Automath languages, during his work in the project Mathematical Language Automath (under supervision of Prof. de Bruijn) at the Eindhoven University of Technology. These studies can be considered as a continuation and completion to previously published work; see [Nederpelt 73 (C3)] and [de Vrijer 75 (C.4)]. Actually, an introduction to the remaining chapters of the thesis is hardly necessary because they are formally self-contained and provided with lengthy introductions themselves. However, we like to make some general remarks on the Automath project, hoping to clarify some points which have sometimes given rise to misunderstanding. Most views expressed are common in the Automath project, but some are personal views, not necessarily shared by other workers in the project. We start with preliminary remarks, followed by a survey of the Automath project. We discuss the language theory and its role in the project. We give an informal introduction to the various Automath languages and explain how mathematical reasoning can be represented. Finally we summarize the contents of this thesis. Occasionally we make a comparison with related logical systems and related enterprises elsewhere. For more information on the subjects of this chapter we refer to [de Bruijn 80 (A.5)], [van Benthem Jutting 77], [Zucker 77 (A.~)] and [van Daalen 73 (A.3)].
    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 I, Sections 1-5 (Introduction)'. Together they form a unique fingerprint.

    Cite this