謂詞邏輯 (Predicate Logic)
邏輯推論簡介布林邏輯皮諾公設系統一階邏輯完備定理不完備定理程式實作布林推論一階推論相關訊息相關網站相關書籍參考文獻最新修改訊息相關網站參考文獻最新修改簡體版English |
簡介布林邏輯、謂詞邏輯與一階邏輯是最常被使用的兩種邏輯系統，布林邏輯在電路設計上有強大的用途，而一階邏輯則成為人工智慧領域的理論基礎。 謂詞邏輯乃是布林邏輯的延伸，此種邏輯具有一種類似布林函數的基本元素，通常稱為謂詞 (Predicate)，因此稱為謂詞邏輯 (Predicate Logic) 。 一階邏輯乃是謂詞邏輯的延伸，包含兩個很特別的量詞運算，全部 (forall) 與存在 (exist) 等，如果我們不處理這兩個運算，則將退化為謂詞邏輯。 謂詞邏輯的推論謂詞邏輯的推論法則有很多種，在此我們使用最簡單且強大的羅氏 (Robinson) 推論法則，利用解析法 (Resolution) 進行推論。 我們設計了一個一階邏輯的推論器，用來對這種較弱的謂詞邏輯進行推論，以下 Java 程式片段是其推論引擎的核心。 /**@param pRules Example : "a(X,Y)|-p(X,Y);a(X,Y)|-p(X,Z)|-a(Z,Y);p(a,b);p(b,c)".split(";") *@return Example : "a(a,b);a(b,c);a(a,c);" */ public static String unitResolution(String[] pRules) { Vector rules = new Vector(Arrays.asList(pRules)); for (int ri=0; ri<rules.size(); ri++) { String rule1 = (String) rules.get(ri); if (rule1.indexOf("|")>0) continue; // it's not a unit rule String negTerm1 = negate(rule1); // negate the unit rule String negTag = STR.head(negTerm1, "("); for (int rj=0; rj<rules.size(); rj++) { String rule2 = (String) rules.get(rj); // ex : unify e(a) with b(a),-d(a),-e(a) => b(a),-d(a) String[] terms2 = rule2.split("\\|"); // terms2 = {-e(X)} for (int ti=0; ti<terms2.length; ti++) { String tag = STR.head(terms2[ti], "("); if (!tag.equals(negTag)) continue; String unify = unify(negTerm1, terms2[ti]); // unify e(a), -e(X) if (unify == null) continue; String bindRule = STR.expand(rule2, unify); // b(X),-d(X),-e(X) => b(a),-d(a),-e(a) String unifyRule = STR.replace("|"+bindRule+"|", "|"+negTerm1+"|", "|"); // ,b(a),-d(a),-e(a), => ,b(a),-d(a) unifyRule = STR.trim(unifyRule, '|'); // ,b(a),-d(a), => b(a),-d(a) if (rules.indexOf(unifyRule) < 0) { rules.add(unifyRule); System.out.println(rule1+" "+rule2+"\r\n ["+unify+"] => "+unifyRule); } } } } StringBuffer facts = new StringBuffer(); for (int ri=pRules.length; ri<rules.size(); ri++) { String rule = (String) rules.get(ri); if (rule.indexOf("|") < 0) facts.append(rule+";"); } return facts.toString(); } 結語羅氏的謂詞邏輯推論法具有理論上的重要性，既簡單又優美，本文對該方法進行了一個簡易的實作，雖然不夠完整，但希望能清楚的說明其原理。 |
page revision: 1, last edited: 11 Sep 2010 00:42
Post preview:
Close preview