计算机逻辑

计算机逻辑描述应用于计算机科学人工智能逻辑。它包括:

  • 以在计算机科学中的应用为导向的逻辑学研究。例如:组合子逻辑抽象释义
  • 以逻辑形式自然表达的计算机科学基本概念。例如:编程语言的形式语义霍尔逻辑逻辑编程
  • 计算理论的关注形式逻辑的基本问题的方面。例如:Curry-Howard对应博弈语义
  • 被当作应用计算机科学的逻辑工具。例如:自动定理证明模型效验
  • 软件(和硬件)开发的形式方法,比如在Z符号中使用谓词逻辑

基本数理逻辑比如命题逻辑谓词逻辑(通常联合上集合论)的研究被认为是对任何大学计算机科学课程都非常重要的理论基础。高阶逻辑通常不教,但在定理证明工具如HOL中是很重要的。

有相关的一个年刊IEEE Symposium on Logic in Computer Science(LICS)。

书籍