分类:计算机逻辑

计算机逻辑是数理逻辑的一个分支，它大致上是逻辑学和计算机科学的交集。它包括:

1. 以在计算机科学中的应用为导向的逻辑学研究。例如:
   • 组合子逻辑和抽象释义;
2. 以逻辑形式自然表达的计算机科学基本概念。例如:
   • 编程语言的形式语义, Hoare逻辑, 和逻辑编程;
3. 从关注纯逻辑学问题的计算理论推导出来的基本概念的应用。例如:
   • Curry-Howard对应和博弈语义;
4. 被当作应用计算机科学的逻辑工具。例如:
   • 自动定理证明和模型检查。