計(jì)算機(jī)邏輯描述應(yīng)用于計(jì)算機(jī)科學(xué)和人工智能的邏輯。

中文名

計(jì)算機(jī)邏輯

類型

邏輯

領(lǐng)域

計(jì)算機(jī)

應(yīng)用

計(jì)算機(jī)科學(xué)和人工智能

正文

它包括:

以在計(jì)算機(jī)科學(xué)中的應(yīng)用為導(dǎo)向的邏輯學(xué)研究。例如: 組合子邏輯和抽象釋義;

以邏輯形式自然表達(dá)的計(jì)算機(jī)科學(xué)基本概念。例如: 編程語(yǔ)言的形式語(yǔ)義, Hoare 邏輯, 和邏輯編程;

計(jì)算理論的關(guān)注形式邏輯的基本問(wèn)題的方面。例如: Curry-Howard對(duì)應(yīng)和博弈語(yǔ)義;

被當(dāng)作應(yīng)用計(jì)算機(jī)科學(xué)的邏輯工具。例如:自動(dòng)定理證明和模型效驗(yàn)。

軟件(和硬件)開(kāi)發(fā)的形式方法,比如在Z符號(hào)中使用謂詞邏輯。

基本數(shù)理邏輯比如命題邏輯和謂詞邏輯(通常聯(lián)合上集合論)的研究被認(rèn)為是對(duì)任何大學(xué)計(jì)算機(jī)科學(xué)課程都非常重要的理論基礎(chǔ)。高階邏輯通常不教,但在定理證明工具如HOL中是很重要的。

有相關(guān)的一個(gè)年刊IEEE Symposium on Logic in Computer Science (LICS)。