Simple Type Theory: A Practical Logic for Expressing and Reasoning about Mathematical Ideas
暫譯: 簡單類型理論：表達和推理數學思想的實用邏輯
Farmer, William M.
- 出版商: Springer
- 出版日期: 2023-01-02
- 售價: $3,790
- 貴賓價: 9.5 折 $3,601
- 語言: 英文
- 頁數: 295
- 裝訂: Hardcover - also called cloth, retail trade, or trade
- ISBN: 3031211111
- ISBN-13: 9783031211119
-
相關分類:
邏輯設計 Logic-design
海外代購書籍(需單獨結帳)
相關主題
商品描述
The book is an introduction to simple type theory, a classical higher-order version of predicate logic that extends first-order logic. It presents a practice-oriented logic called Alonzo that is based on Alonzo Church's formulation of simple type theory known as Church's type theory. Unlike traditional predicate logics, Alonzo admits undefined expressions. The book illustrates, using Alonzo, how simple type theory is suited ideally for reasoning about mathematical structures and constructing libraries of mathematical knowledge.
Topics and features:
- Offers the first book-length introduction to simple type theory as a predicate logic
- Provides the reader with a logic that is close to mathematical practice
- Presents the tools needed to build libraries of mathematical knowledge
- Employs two semantics, one for mathematics and one for logic
- Emphasizes the model-theoretic view of predicate logic
- Includes several important topics, such as definite description and theory morphisms, not usually found in standard logic textbooks
Aimed at students of computing and mathematics at the graduate or upper-undergraduate level, this book is also well-suited for mathematicians, computing professionals, engineers, and scientists who need a practical logic for expressing and reasoning about mathematical ideas.
William M. Farmer is a Professor in the Department of Computing and Software at McMaster University in Hamilton, Ontario, Canada.
商品描述(中文翻譯)
這本獨特的教科書與標準邏輯教材不同，提供讀者一種可以在實踐中實際使用的邏輯，以表達和推理數學概念。
本書是對簡單類型理論的介紹，這是一種經典的高階謂詞邏輯版本，擴展了第一階邏輯。它呈現了一種以Alonzo為名的實踐導向邏輯，基於阿隆佐·丘奇（Alonzo Church）所提出的簡單類型理論，即丘奇的類型理論。與傳統的謂詞邏輯不同，Alonzo 接納未定義的表達式。本書使用 Alonzo 說明簡單類型理論如何理想地適用於數學結構的推理以及構建數學知識庫。
主題與特點：
- 提供了對簡單類型理論作為謂詞邏輯的首次書籍長度介紹
- 為讀者提供接近數學實踐的邏輯
- 呈現構建數學知識庫所需的工具
- 使用兩種語義，一種用於數學，另一種用於邏輯
- 強調謂詞邏輯的模型理論觀點
- 包括幾個重要主題，如確定描述和理論同態，這些主題通常不會出現在標準邏輯教科書中
本書針對計算機和數學的研究生或高年級本科生，對於需要一種實用邏輯來表達和推理數學概念的數學家、計算專業人士、工程師和科學家也非常合適。
William M. Farmer 是加拿大安大略省漢密爾頓市麥克馬斯特大學計算與軟體系所的教授。
作者簡介
Dr. Farmer's research interests are logic, mechanized mathematics, mathematical knowledge management, and formal methods. One of his most significant achievements is the design and implementation of the IMPS proof assistant, which was done at MITRE in partnership with Dr. Joshua Guttman and Dr. Javier Thayer. His work on IMPS has lead to research on developing practice-oriented logics and set theories and on organizing mathematical knowledge as a network of interconnected axiomatic theories. He and Dr. Jacques Carette are currently leading the MathScheme project at McMaster with the aim of developing a framework for integrating axiomatic and algorithmic mathematics. On this project Dr. Farmer has focused on how to reason about the interplay of syntax and semantics, as exhibited in syntax-based mathematical algorithms like symbolic differentiation, within a logic equipped with global quotation and evaluation operators. Dr. Farmer has had a career-long interest in using simple type theory as a practical logic for expressing and reasoning about mathematical ideas. He is the author of "The Seven Virtues of Simple Type Theory", Journal of Applied Logic, 6:267-286, 2008, one of the leading references on simple type theory.
作者簡介(中文翻譯)
威廉·M·法默在計算和數學領域擁有超過35年的產業和學術經驗。他於1978年在聖母大學獲得數學學士學位，1980年獲得數學碩士學位，1983年獲得計算機科學碩士學位，並於1984年在威斯康辛大學麥迪遜分校獲得數學博士學位。他目前是麥克馬斯特大學計算與軟體系所的教授。在1999年加入麥克馬斯特之前，他在美國麻薩諸塞州貝德福德的MITRE公司從事了十二年的計算機科學研究，並在聖克勞德州立大學教授了兩年的計算機程式設計和網路課程。
法默博士的研究興趣包括邏輯、機械化數學、數學知識管理和形式方法。他最重要的成就之一是設計和實現IMPS證明助手，這項工作是在MITRE與喬舒亞·古特曼博士和哈維爾·泰爾博士的合作下完成的。他在IMPS上的工作促進了針對實踐導向邏輯和集合論的研究，以及將數學知識組織為相互連結的公理理論網絡。他和雅克·卡雷特博士目前在麥克馬斯特大學領導MathScheme專案，旨在開發一個整合公理數學和演算法數學的框架。在這個專案中，法默博士專注於如何推理語法和語義之間的相互作用，這在基於語法的數學演算法（如符號微分）中得以體現，並且在具備全域引用和評估運算子的邏輯中進行探討。法默博士在其職業生涯中一直對使用簡單類型理論作為表達和推理數學思想的實用邏輯感興趣。他是《簡單類型理論的七個美德》的作者，該文發表於《應用邏輯期刊》，6:267-286，2008年，是簡單類型理論的主要參考文獻之一。
