另一個非常高效的專用推理系統(tǒng)與等價性推理相關(guān)。直接將等價性作為公理放到定理證明系統(tǒng)中是很難的。這是因為，對同一個對象而言如果只是使用兩個不同的名字，將很難表示出兩個不同但等價的公式。但是，有一種有效的算法，能夠記錄基于等價類的基項之間的等價信息。如果這些技術(shù)能夠集成到合一程序中，就不需要直接將等價性作為公理寫到系統(tǒng)中。相反，擴展的合一算法將用等價程序來檢查兩個項是否等價并進而合一。

其他幾種專用的推理系統(tǒng)可以這樣實現(xiàn)：在系統(tǒng)中集成某些專門定義的程序，這些程序用來確定一些特定謂詞的真值。這種技術(shù)稱為附屬程序。例如，思考一下時間的推理。雖然可以用時間公理化來驅(qū)動時間性的推理，但這樣的系統(tǒng)效率很低。有些專門的推理技術(shù)能有效地管理時間信息，因此可以作為特殊的謂詞集成到綜合系統(tǒng)中。為了理解這一點，我們分析命題在一個推理系統(tǒng)中充當(dāng)?shù)慕巧?。一般有三種不同的操作可應(yīng)用于命題：

斷言為真（即，將其添加到KB中）

查詢它是否為真（即，激活定理證明程序來加以驗證）

撤銷它（即，將其從知識庫中刪除）

雖然每個操作都是用定理證明系統(tǒng)中的術(shù)語來定義的，但這并不表示它是完成這些操作的惟一途徑。事實上，可以定義任意過程來執(zhí)行每一個任務(wù)。例如，考慮一個特定的時間推理系統(tǒng)，它維護一個時間關(guān)系圖，并使用圖搜索技術(shù)來構(gòu)建時間關(guān)系。假定知識庫中有一個謂詞“BEFORE”，表示一個時間在另一個之前。當(dāng)命題（BEFORE t1 t2）加到知識庫中時，這個特定的時間推理過程就被激活，并將信息加到時間圖中去。在查詢同樣的命題時（或者是直接由用戶提出的查詢，或者是一個復(fù)雜證明過程的其中一步)，系統(tǒng)就調(diào)用該特定的時間推理過程來進行構(gòu)造。這樣，這個專用的時間推理程序就完全集成到定理證明程序中，并且一旦需要時間性信息時就會調(diào)用。當(dāng)然，要完全集成起來，這種專用的推理還要能處理變量并返回與合一等價的結(jié)果。例如，定理證明程序需要構(gòu)造(BEFORE t1 ?x)，那么時間推理程序就要返回一個對?x的約束。除此之外，當(dāng)需要尋找另一個答案時，還要能處理回溯。

為將專用的推理算法集成到統(tǒng)一的框架中，綜合推理系統(tǒng)提供了一種很有吸引力的方法。

責(zé)任編輯：admin