数理逻辑

2022年10月14日 (五) 06:31的版本

您可以在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

项目

• Prolog logic programming language
• Proof assistant
• 定理证明/公式推导

课程

• Formal Reasoning course notes
• Pure and Applied Logic (PAL) program at Carnegie Mellon University
• Propositional logic and First-order logic 有完整的幻灯片资料供下载

文档

书籍

• 《Simply Logical Intelligent Reasoning by Example》 (Fully Interactive Online Edition)
• 《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