一階邏輯的推論 -- 程式實作

訊息

參考文獻

簡體版

English

程式內容

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
      String negTag   = 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 = 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  = 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) {
            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();
  }
 
  /** 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 name   = head(macros[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);

Facebook

code java logic

page revision: 4, last edited: 03 Nov 2010 02:21

Edit Rate (0) Tags Discuss (0) History Files Print Site tools + Options

金門大學：免費電子書、教材、程式、動畫

訊息

程式內容

執行結果

Facebook

Facebook

Wikidot

Post preview:

Other interesting sites