欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜：Formal mathematics/Isabelle/ML, Formal verification/Coq/Agda, C++/Erlang/Lisp
数理逻辑
来自开放百科 - 灰狐
（版本间的差异）
小 (→书籍) |
小 (→简介) |
||
| 第4行： | 第4行： | ||
==简介== | ==简介== | ||
| − | 数理逻辑（Mathematical logic）是数学的一个分支，其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑是数学基础的一个不可缺少的组成部分。 | + | 数理逻辑（Mathematical logic）是数学的一个分支，其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑是数学基础的一个不可缺少的组成部分。 |
| + | |||
| + | 在逻辑和数学里，命题演算（或称句子演算）是一个形式系统，有着可以由以逻辑运算符结合原子命题来构成代表“命题”的公式，以及允许某些公式建构成“定理”的一套形式“证明规则”。 | ||
==历史== | ==历史== | ||
2022年10月10日 (一) 00:09的版本
|
您可以在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
文档
书籍
- 《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
图集
命题逻辑的符号
基本符号
链接
分享您的观点
