布林邏輯 (Boolean Logic)

邏輯推論 簡介 布林邏輯 皮諾公設系統 一階邏輯 完備定理 不完備定理 程式實作 布林推論 一階推論 相關訊息 相關網站 相關書籍 參考文獻 最新修改 訊息 相關網站 參考文獻 最新修改 簡體版 English

文章 簡介 布林邏輯在電路設計上有強大的用途，是最簡單的邏輯系統，由於是喬治、布林(George Boole)所建立的基礎理論，因此被稱為布林邏輯。 布林所提出的真值表，是布林邏輯中最基礎也最重要的方法，在布林邏輯中，每個值都只能是真的或假的，不可以是其他值。這種非真即假的特性，稱為「排中律」，我們可以將「排中律」寫成下列公式。 P | -P => true // P 或 -P 中必然有一者為真。 推論法則 要用布林邏輯來進行推論，必須依靠所謂的推理方法，亞里斯多德 (Aristotle)、希爾伯特 (Hilbert)、洪氏 (Horn)、簡森 (Gentzen) 與羅賓遜 (Robinson) 前後對這些推論方法進行了關鍵性的研究，其中、最簡單且功能強大的莫過於羅氏 (Robinson) 的解析法 (Resolution) 了。 關於布林邏輯的進一步訊息，請參看下列兩份投影片。 LogicIntroduction.ppt — http://www.scribd.com/doc/20974598/Logic-Introduction LogicReasoning.ppt — http://www.scribd.com/doc/20974606/Logical-Reasoning 然而，純粹的解析法並不完備，要利用羅氏的解析法證明任意問題，必須使用反證法 (Refutation)，其方法是將待證明語句 P 的反向句 -P 加入到規則庫當中，如果可以導出矛盾 (假值)，則代表該語句 P 被證實。 根據 Horn 的前向推論法與 Robinson 的 Refutation 方法，我們用 Java 寫了一個推理引擎，其程式碼位於 BooleanLogic.java 中，該程式中的 unitResolution() 函數是採用 Robinson 的推論法則，而 hornReasoning() 函數則採用 Horn 的推論法則，兩者的程式碼分別如下。 洪式推論法 (Horn Clause Reasoning) public static void hornReasoning(String[] rules) { TreeMap trueMap = new TreeMap(); int satisfyRuleCount; do { satisfyRuleCount = 0; for (int ri=0; ri<rules.length; ri++) { if (rules[ri].length() == 0) continue; String head = STR.head(rules[ri], "<-"); String body = STR.tail(rules[ri], "<-"); String[] conds = body.split(","); boolean isSatisfy = true; for (int ci=0; ci<conds.length; ci++) { if (conds[ci].length() == 0) continue; if (trueMap.get(conds[ci]) == null) isSatisfy = false; } if (isSatisfy) { System.out.println(rules[ri]); trueMap.put(head, "1"); rules[ri] = ""; satisfyRuleCount ++; } } } while (satisfyRuleCount > 0); } 羅式的推論法 (Robinson's Resolution Reasoning) public static void unitResolution(String[] pRules) { Vector rules = new Vector(); for (int ri=0; ri<pRules.length; ri++) rules.add(rewrite(pRules[ri])); for (int ri=0; ri<rules.size(); ri++) { String rule1 = (String) rules.get(ri); if (rule1.indexOf(",")>0) continue; // it's not unit rule. String term = rule1; String negTerm = neg(term); for (int rj=0; rj<rules.size(); rj++) { String rule2 = (String) rules.get(rj); String exp = ","+rule2+","; if (exp.indexOf(","+negTerm+",")>0) { String unifyExp = STR.replace(exp, ","+negTerm+",", ","); String newRule = unifyExp.substring(1, unifyExp.length()-1); rules.add(newRule); System.out.println("unfiy("+rule1+"|"+rule2+")="+newRule); } } } } 結語 布林邏輯雖然是一種簡單的邏輯系統，但其數學基礎非常紮實，是西洋文化的精隨之所在。如果我們能欣賞這種邏輯系統的美麗之處，那麼將能理解西方數學的重要性，進而將其應用到電腦領域，發展出更好的人工智慧程式。 Facebook 留言 Facebook Wikidot Post preview: Close preview or Sign in as Wikidot user (will not be published) - + Help: wiki text quick reference 授權 本網頁的作者、授權與引用方式 作者 陳鍾誠，於金門大學資訊工程系，電子郵件：wt.ude.uqn|ccc#wt.ude.uqn|ccc，網站：http://ccckmit.wikidot.com。 授權 本文採用創作共用 (Creative Common) 3.0 版的 姓名標示─非商業性─相同方式分享 授權條款，歡迎轉載或修改使用，但若做為商業使用時必須取得授權，引用本文時請參考下列格式。 中文版 (APA格式) 陳鍾誠 (13 Oct 2009 02:12)，(網頁標題) 布林邏輯 (Boolean Logic)，(網站標題) 陳鍾誠的網站，取自 http://ccckmit.wikidot.com/lr:booleanlogic1 ，網頁修改第 9 版。 英文版 (APA格式) Chung-Chen Chen (13 Oct 2009 02:12), Retrieved from http://ccckmit.wikidot.com/lr:booleanlogic1 , Page Revision 9.