# 程式內容

```import java.util.*;

public class FirstOrderLogic {
/** A test example for FirstOrderLogic */
public static void main(String[] args) {
String ruleList = "a(X,Y)|-p(X,Y);a(X,Y)|-p(X,Z)|-a(Z,Y);p(a,b);p(b,c)";
System.out.println("facts : "+ruleList);
String newFacts = unitResolution(ruleList.split(";"));
System.out.println("inference : "+newFacts);
}
/** Example : negate("p(x)") => "-p(x)" */
public static String negate(String pTerm) {
if (pTerm.startsWith("-"))
return pTerm.substring(1);
else
return "-"+pTerm;
}
/**@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
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++) {
if (!tag.equals(negTag)) continue;
String unify = unify(negTerm1, terms2[ti]);              // unify e(a), -e(X)
if (unify == null) continue;
String bindRule  = expand(rule2, unify);               // b(X),-d(X),-e(X) => b(a),-d(a),-e(a)
String unifyRule = replace("|"+bindRule+"|", "|"+negTerm1+"|", "|"); // ,b(a),-d(a),-e(a), => ,b(a),-d(a)
unifyRule = trim(unifyRule, '|');                 // ,b(a),-d(a), => b(a),-d(a)
if (rules.indexOf(unifyRule) < 0) {
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();
}

/** add rule into rules */
public static void addRule(String rule, Vector rules) {
}

/** Example : type("X") => "var";  type("a") => "value"; */
public static String type(String pToken) {
if (Character.isUpperCase(pToken.charAt(0))) return "var"; else return "value";
}

/** Example : unify("p(X,Y)", "p(a,b)") => "X=a|Y=b" */
public static String unify(String term1, String term2) {
StringBuffer rzUnify = new StringBuffer();
String body1 = innerText(term1, "(", ")");
String body2 = innerText(term2, "(", ")");
String[] params1 = body1.split(",");
String[] params2 = body2.split(",");
if (params1.length != params2.length) return null;
for (int i=0; i<params1.length; i++) {
String type1 = type(params1[i]);
String type2 = type(params2[i]);
if (type2.equals("var") && type1.equals("value"))  // ex : parent(john,johnson)/parent(X, johnson) => X/john
rzUnify.append("|"+params2[i]+"="+params1[i]);
if (type1.equals("value")&&type2.equals("value"))  // ex : parent(X,mary)/parent(X,bob) => fail
if (!params1[i].equals(params2[i]))
return null;
}
if (rzUnify.length() == 0) return null;
return rzUnify.substring(1);
}

public static String innerText(String pXml, String beginMark, String endMark) {
int beginStart = pXml.indexOf(beginMark);
if (beginStart < 0) return null;
int beginEnd = beginStart+beginMark.length();
int endStart = pXml.indexOf(endMark, beginEnd);
if (endStart < 0) return null;
return pXml.substring(beginEnd, endStart);
}
public static String head(String pStr, String pSpliter) {
int spliterPos = pStr.indexOf(pSpliter);
if (spliterPos < 0) return pStr;
return pStr.substring(0,spliterPos);
}

public static String tail(String pStr, String pSpliter) {
int spliterPos = pStr.indexOf(pSpliter);
if (spliterPos < 0) return "";
return pStr.substring(spliterPos+pSpliter.length());
}

public static String expand(String pText, String pMacros) {
String[] macros = pMacros.split("\\|");
for (int i=0; i<macros.length; i++) {
String expand = tail(macros[i], "=");
pText = replace(pText, name, expand);
}
return pText;
}

public static String replace(String pStr, String fromPat, String toPat) {
if (fromPat.length()==0) return pStr;
if (pStr.indexOf(fromPat)<0) return pStr;
StringBuffer rzStr = new StringBuffer();
int strIdx = 0, nextIdx;
while ((nextIdx = pStr.indexOf(fromPat, strIdx))>=0) {
rzStr.append(pStr.substring(strIdx, nextIdx));
rzStr.append(toPat);
strIdx = nextIdx + fromPat.length();
}
rzStr.append(pStr.substring(strIdx));
return rzStr.toString();
}

public static String trim(String pStr, char pChar) {
int begin, end;
for (begin=0; begin<pStr.length(); begin++)
if (pStr.charAt(begin) != pChar) break;
for (end = pStr.length()-1; end>0; end--)
if (pStr.charAt(end) != pChar) break;
return pStr.substring(begin, end+1);
}
}
```

# 執行結果

``````D:\wikidot\LR>javac FirstOrderLogic.java
Note: FirstOrderLogic.java uses unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.

D:\wikidot\LR>java FirstOrderLogic
facts : a(X,Y)|-p(X,Y);a(X,Y)|-p(X,Z)|-a(Z,Y);p(a,b);p(b,c)
p(a,b)  a(X,Y)|-p(X,Y)
[X=a|Y=b] => a(a,b)
p(a,b)  a(X,Y)|-p(X,Z)|-a(Z,Y)
[X=a|Z=b] => a(a,Y)|-a(b,Y)
p(b,c)  a(X,Y)|-p(X,Y)
[X=b|Y=c] => a(b,c)
p(b,c)  a(X,Y)|-p(X,Z)|-a(Z,Y)
[X=b|Z=c] => a(b,Y)|-a(c,Y)
a(a,b)  a(X,Y)|-p(X,Z)|-a(Z,Y)
[Z=a|Y=b] => a(X,b)|-p(X,a)
a(b,c)  a(X,Y)|-p(X,Z)|-a(Z,Y)
[Z=b|Y=c] => a(X,c)|-p(X,b)
a(b,c)  a(a,Y)|-a(b,Y)
[Y=c] => a(a,c)
a(a,c)  a(X,Y)|-p(X,Z)|-a(Z,Y)
[Z=a|Y=c] => a(X,c)|-p(X,a)
inference : a(a,b);a(b,c);a(a,c);```
```