Thirty Five Years of Automating Mathematics
THIRTY FIVE YEARS OF AUTOMATING MATHEMATICS: DEDICATED TO 35 YEARS OF DE BRUIJN'S AUTOMATH N. G. de Bruijn was a well established mathematician before deciding in 1967 at the age of 49 to work on a new direction related to Automating Mathematics. By then, his contributions in mathematics were n...
| Other Authors: | |
|---|---|
| Format: | eBook |
| Language: | English |
| Published: |
Dordrecht
Springer Netherlands
2003, 2003
|
| Edition: | 1st ed. 2003 |
| Series: | Applied Logic Series
|
| Subjects: | |
| Online Access: | |
| Collection: | Springer Book Archives -2004 - Collection details see MPG.ReNa |
Table of Contents:
- A Mathematical Model for Biological Memory and Consciousness
- Towards an Interactive Mathematical Proof Mode
- Recent Results in Type Theory and their Relationship to Automath
- Linear Contexts, Sharing Functors: Techniques for Symbolic Computation
- De Bruijn’s Automath and Pure Type Systems
- Hoare Logic with Explicit Contexts
- Transitive Closure and the Mechanization of Mathematics
- Polymorphic Type-checking for the Ramified Theory of Types of Principia Mathematica
- Termination in ACL2 using Multiset Relations
- The ?-Calculus in FM
- Proof Development with ?mega: The Irrationality of % MathType!MTEF!2!1!+- % feaagCart1ev2aaatCvAUfeBSjuyZL2yd9gzLbvyNv2CaerbuLwBLn % hiov2DGi1BTfMBaeXatLxBI9gBaerbd9wDYLwzYbItLDharqqtubsr % 4rNCHbGeaGqiVu0Je9sqqrpepC0xbbL8F4rqqrFfpeea0xe9Lq-Jc9 % vqaqpepm0xbba9pwe9Q8fs0-yqaqpepae9pg0FirpepeKkFr0xfr-x % fr-xb9adbaqaaeGaciGaaiaabeqaamaabaabaaGcbaWaaOaaaeaaca % aIYaaaleqaaaaa!36CB!]]