欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜：Formal mathematics/Isabelle/ML, Formal verification/Coq/Agda, C++/Erlang/Lisp
数理逻辑
来自开放百科 - 灰狐
（版本间的差异）
小 (→文档) |
小 (→体系) |
||
| 第10行： | 第10行： | ||
==体系== | ==体系== | ||
数理逻辑的主要分支包括：模型论、证明论、递归论和公理化集合论。 | 数理逻辑的主要分支包括：模型论、证明论、递归论和公理化集合论。 | ||
| + | |||
| + | [http://logic.cmu.edu/ 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 | ||
==项目== | ==项目== | ||
2022年10月7日 (五) 04:57的版本
|
您可以在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
项目
课程
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
图集
命题逻辑的符号
基本符号
链接
分享您的观点
