KM全名是知識機器（Knowledge Machine），KM有一階邏輯的語意，也有包括依描述選擇、合一、分類、理解等機械推理，KM源自Theo語言及KRL 程式語言（KRL (programming language)），是用Lisp實現。KM程式語言是用在知識表示領域的知識框架語言。
基本介紹
- 中文名：KM程式語言
- 外文名：Knowledge Machine programming language
- 學科：人工智慧
- 定義：用在知識表示領域的知識框架語言
- 有關術語：知識表示
- 領域：本體語言
簡介,聲明式編程,知識表達,推理規則,
簡介
在人工智慧領域，KM程式語言是一種本體語言，用於知識表示的本體的形式語言。此類語言允許對有關特定領域的知識加以編碼，且常常還包括為處理這些知識提供支持的推理規則。常為描述性語言（又稱為表述型語言、說明性語言），幾乎總是屬於框架語言的泛化形式，且一般都基於一階邏輯或描述邏輯。
聲明式編程
聲明式編程（Declarative programming）是一種編程範式，與命令式編程相對立。它描述目標的性質，讓計算機明白目標，而非流程。聲明式編程不用告訴計算機問題領域，從而避免隨之而來的副作用。而命令式編程則需要用算法來明確的指出每一步該怎么做。
聲明式編程通常被看做是形式邏輯的理論，把計算看做推導。聲明式編程因大幅簡化了並行計算的編寫難度，自2009起備受關注。
聲明式語言包包括資料庫查詢語言（SQL，XQuery），正則表達式，邏輯編程，函式式編程和組態管理系統。聲明式編程透過函式、推論規則或項重寫（term-rewriting）規則，來描述變數之間的關係。它的語言運行器（編譯器或解釋器）採用了一個固定的算法，以從這些關係產生結果。
聲明式程式語言通常用作解決人工智慧和約束滿足問題。聲明式編程通常被定義為除命令式以外的編程範式。同時存在一些其他的定義，這些定義不是簡單的將聲明式編程和命令式編程做對比，例如：
- 聲明式編程是告訴計算機需要計算“什麼”而不是“如何”去計算
- 任何沒有副作用的程式語言，或者更確切一點，任何引用透明的程式語言
- 任何有嚴格計算邏輯的程式語言
這些定義有一些是重合的。
知識表達
知識的形式化表達。它能使計算機利用知識進行智慧型信息處理。描述外部世界所作出的一組約定，是使知識符號化並傳送給計算機的過程。
研究知識從自然記載形式轉變成適合於計算機處理的表示形式。知識表示一般應具有下列特性：
- 廣泛的知識表示能力，具有直接描述問題世界的表示能力，可表示具有結構的知識、不完全的知識以及元知識等；
- 模組性，便於知識的追加、修正及階段性擴展；
- 易於管理，易檢測出矛盾的知識、冗餘的知識等，以維護知識庫的一致性；
- 易於人們理解；
- 與高效的推理方法相配合，例如應具有聯想功能等。
知識的表示方法大體上可分為過程型表示法和陳述型表示法兩大類。過程型表示法是根據要解決的特定問題，指出一系列操作過程的表示方法，其執行效率高，但適應性差。陳述型表示法是將事實和判斷規則分別加以說明的表示方法，它可用知識表示相互獨立的事物，易於追加、修正，具有較好的通用性和適應性，但處理問題的效率較低。使用的具有代表性的知識表示方法大致有以下幾種：
- 產生式系統，用產生式規則來表示知識的專家系統；
- 黑板模型，不同層次、不同類的知識源，通過被稱為黑板的公用數據區而得到協調的處理；
- 框架系統，按照框架理論建立的知識表示模型；
- 謂詞邏輯，用邏輯式的集合來記述知識，並含有謂詞邏輯的推理功能，如基於歸結原理的演繹推理機能；
- 語義網路，由結點和連結結點的有向弧構成，具有對網路進行搜尋和操作的算法；
- 對象模型，是表達以解決知識庫的問題為對象的系統及概念的模型，能某種程度地使用深層知識；
- 上述幾種方法的某種組合。
推理規則
在邏輯中，特別是數理邏輯中，推理規則（推論規則）是構造有效推論的方案。這些方案建立在一組叫做前提的公式和叫做結論的斷言之間的語法關係。這些語法關係用於推理過程中，新的真的斷言從其他已知的斷言得出。規則也適用於非形式邏輯和邏輯論證，但是形式化更加困難和有爭議。
按照規定，推理規則的套用純粹是語法過程。儘管如此它必須是有效的，或者更精確地說保持有效性。為了使保持有效性的要求有意義，某種形式的語義與推理規則有關和推理規則自身的斷言是必需的。對於在推理規則和和語義之間相互關係的討論請參見命題邏輯。
命題邏輯中推理規則的顯著例子是肯定前件和否定後件規則。對於一階謂詞邏輯，推理規則需要處理邏輯量詞。對這種論證的更詳細的描述請參見有效性。在一階謂詞邏輯中把所有推理規則作為一個單一規則來統一處理請參見一階歸結。
注意有很多不同的形式邏輯系統，每個都帶有合式公式、推理規則和語義的自己的集合。參見時間邏輯、模態邏輯或直覺邏輯的實例。量子邏輯也是一種不同尋常形式的邏輯。參見證明論。在謂詞演算中，需要一個補充的推理規則。它叫做普遍化。
