Thirty Five Years of Automating Mathematics
By: edited by Fairouz D. Kamareddine
Series: Applied Logic Series -- 28; Applied Logic Series -- 28
Publisher: Springer Netherlands
Published: 2003
Place of publication: Dordrecht
Language: eng
Format: [electronic resource] /
Number of pages: 320
ISBN-13: 9789048164400; 9789401702539
Subjects: Symbolic and mathematical Logic; Computer science; Data processing; Algebra; Mathematics; Mathematical optimization
Description: This volume is a collection of papers with a personal flavour. It consists of 11 articles which propose interesting variations to or examples of mechanising mathematics and illustrate differ developments in symbolic computation in the past 35 years. The volume further includes a strong argumentation by Arnon Avron that for automated reasoning, there is an interesting logic, somewhere strictly between first and second order logic, determined essentially by an analysis of transitive closure, yielding induction; and Murdoch Gabbay presenting an interesting generalisation of Fraenkel-Mostowski (FM) set theory within higher-order logic, and applying it to model Milner's p calculus.
Notes: Online full text is restricted to subscribers.

Also available in print.

Mode of access: World Wide Web.
Table of contents: title: Contributors. Editorial Preface; title: A Mathematical Model for Biological Memory and Consciousness; title: Towards an Interactive Mathematical Proof Mode; title: Recent Results in Type Theory and their Relationship to Automath; title: Linear Contexts, Sharing Functors: Techniques for Symbolic Computation; title: De Bruijn's Automath and Pure Type Systems; title: Hoare Logic with Explicit Contexts; title: Transitive Closure and the Mechanization of Mathematics; title: Polymorphic Type-checking for the Ramified Theory of Types of Principia Mathematica; title: Termination in ACL2 using Multiset Relations; title: The pi-Calculus in FM; title: Proof Development with Omegamega: The Irrationality of SQRT2; title: Index.