分類:計算機邏輯

計算機邏輯是數理邏輯的一個分支，它大致上是邏輯學和計算機科學的交集。它包括:

1. 以在計算機科學中的應用為導向的邏輯學研究。例如:
   • 組合子邏輯和抽象釋義;
2. 以邏輯形式自然表達的計算機科學基本概念。例如:
   • 程式語言的形式語義, Hoare邏輯, 和邏輯編程;
3. 從關注純邏輯學問題的計算理論推導出來的基本概念的應用。例如:
   • Curry-Howard對應和博弈語義;
4. 被當作應用計算機科學的邏輯工具。例如:
   • 自動定理證明和模型檢查。