162 research outputs found
Relating Proof Systems for Recursive Types
No full textKlop, J.W. [Promotor]Vrijer, R.C. de [Copromotor
Bohm-Like Trees for Rewriting
No full textKlop, J.W. [Promotor]Raamsdonk, F. [Copromotor]Vrijer, R.C. de [Copromotor
The language theory of Automath : Chapter I, Sections 1-5 (Introduction)
No full textThis 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)]
The language theory of Automath : Chapter I, Sections 1-5 (Introduction)
No full textThis 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)]
- …
