数理逻辑

您可以在Wikipedia上了解到此条目的英文信息 数理逻辑 Thanks, Wikipedia.

数理逻辑

简介

数理逻辑（Mathematical logic）是数学的一个分支，其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑是数学基础的一个不可缺少的组成部分。

体系

数理逻辑的主要分支包括：模型论、证明论、递归论和公理化集合论。

Pure and Applied Logic (PAL) 领域包括:

• automated theorem proving
• category theory and categorical logic
• constructive mathematics
• formal verification
• foundations of decision theory
• foundations of programming languages
• homotopy type theory
• logics of programs
• logic in linguistics
• lambda calculus
• learning theory
• model theory
• proof theory
• set theory
• temporal and modal logics
• theory of computing
• type theory

项目

• Proof assistant
• 定理证明/公式推导

课程

Pure and Applied Logic (PAL) program at Carnegie Mellon University

书籍

• 《Homotopy Type Theory: Univalent Foundations of Mathematics》 The Univalent Foundations Program
• 《Practical Foundations For Programming Languages》 Robert Harper, 2016
• 《Type Theory and Functional Programming》 Simon Thompson
• 《An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof》 Peter B. Andrews

图集

• 

  命题逻辑的符号

• 

  基本符号

链接

• From Type Theory to Haskell in 10 Minutes