# 簡介

P | -P => true // P 或 -P 中必然有一者為真。

# 推論法則

1. LogicIntroduction.ppt — http://www.scribd.com/doc/20974598/Logic-Introduction
2. LogicReasoning.ppt — http://www.scribd.com/doc/20974606/Logical-Reasoning

# 洪式推論法 (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 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]);
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++)
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);
System.out.println("unfiy("+rule1+"|"+rule2+")="+newRule);
}
}
}
}```
```