Selected Papers on Automath (eBook)

J.H. Geuvers, R.P. Nederpelt, R.C. de Vrijer (Herausgeber)

eBook Download: PDF

1994 | 1. Auflage
1021 Seiten
Elsevier Science (Verlag)
978-0-08-088718-0 (ISBN)

Infos

The present volume contains a considered choice of the existing literature on Automath. Many of the papers included in the book have been published in journals or conference proceedings, but a number have only circulated as research reports or have remained unpublished. The aim of the editors is to present a representative selection of existing articles and reports and of material contained in dissertations, giving a compact and more or less complete overview of the work that has been done in the Automath research field, from the beginning to the present day. Six different areas have been distinguished, which correspond to Parts A to F of the book. These areas range from general ideas and motivation, to detailed syntactical investigations.

Inhalt

Front Cover 1
Selected Papers on Authomath 4
Copyright Page 5
Contents 12
Preface 8
Hints for the reader 16
Notation 18
Introduction 22
Twenty-five years of Automath research 24
Part A: Motivation and exposition 76
Chapter A.1. Verification of mathematical proofs by a computer 78
Chapter A.2. The mathematical language Automath, its usage, and some of its extensions 94
Chapter A.3. A description of Automath and some aspects of its language theory 122
Chapter A.4. Formalization of classical mathematics in Automath 148
Chapter A.5. A survey of the project Automath 162
Chapter A.6. The language theory of Automath 184
Chapter A.7. Reflections on Automath 222
Chapter A.8. Type systems – basic ideas and applications 250
Part B: Language deflnition and special subjects 270
Chapter B.1. Description of AUT-68 272
Chapter B.2. AUT-SL, a single line version of Automath 296
Chapter B.3. Some extensions of Automath: the AUT-4 family 304
Chapter B.4. AUT-QE without type inclusion 310
Chapter B.5. Checking Landau’s ‘‘Grundlagen” in the Automath system 320
Chapter B.6. The language theory of Automath 324
Chapter B.7. Generalizing Automath by means of a lambda- typed lambda calculus 334
Chapter B.8. Lambda calculus extended with segments 360
Part C: Theory 390
Chapter C.1. A normal form theorem in a .-calculus with types 392
Chapter C.2. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application t o the Church-Rosser theorem 396
Chapter C.3. Strong normalization in a typed lambda calculus with lambda structured types 410
Chapter C.4. Big trees in .-calculus with .-expressions as types 490
Chapter C.5. The language theory of Automath 514
Chapter C.6. The language theory of A infinty, a typed .-calculus where terms are types 676
PART D: Text examples 706
Chapter D.1. Example of a text written in Automath 708
Chapter D.2. Checking Landau’s “Grundlagen” in the Automath system 722
Chapter D.3. Checking Landau’s “Grundlagen” in the Automath system 742
Chapter D.4. A text fragment from Zucker’s “Real Analysis” 754
Chapter D.5. Checking Landau’s “Grundlagen” in the Automath system 784
PART E: Verification 802
Chapter E.1. A verifying program for Automath 804
Chapter E.2. Checking Landau’s “Grundlagen’’ in the Automath system. 826
Chapter E.3. An implementation of substitution in .-calculus with dependent types 830
PART F: Related topics 860
Chapter F.1. Set theory with type restrictions 862
Chapter F.2. Formalisation of constructivity in Authomath 870
Chapter F.3. The Mathematical Vernacular, a language for mathematics with typed sets 886
Chapter F.4. Relational semantics in an integrated system 958
Chapter F.5. Computer program semantics in space and time 968
Bibliography 994
References 996
Indexes 1016
Index of Names 1018
Index of Notations 1024
Index of Subjects 1026

Produkt-Details

• Erscheint lt. Verlag: 20.10.1994
• Sprache: englisch
• Themenwelt: Informatik ► Theorie / Studium ► Algorithmen
• Themenwelt: Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik
• Themenwelt: Mathematik / Informatik ► Mathematik ► Allgemeines / Lexika
• Themenwelt: Mathematik / Informatik ► Mathematik ► Computerprogramme / Computeralgebra
• Themenwelt: Mathematik / Informatik ► Mathematik ► Logik / Mengenlehre
• Themenwelt: Naturwissenschaften
• Themenwelt: Technik
• ISBN-10: 0-08-088718-X / 008088718X
• ISBN-13: 978-0-08-088718-0 / 9780080887180