importjava.util.*;
 
classBooleanLogic{Randomrandom = newRandom();
 
 publicstaticvoidmain(String[]args){Stringrules = "a<-b,c;b<-d,e;c<-d,f;d;e;f";
 hornReasoning(rules.split(";"));
 unitResolution(rules.split(";"));
 }publicstaticStringneg(StringpTerm){if(pTerm.startsWith("-"))returnpTerm.substring(1);
 elsereturn"-"+pTerm;
 }publicstaticStringrewrite(Stringrule){StringBufferrzRule = newStringBuffer();
 Stringhead = head(rule, "<-");
 Stringbody = tail(rule, "<-");
 rzRule.append(head);
 if(body.length() > 0){String[]conds = body.split(",");
 for(inti=0; i<conds.length; i++)rzRule.append(","+neg(conds[i]));
 }returnrzRule.toString();
 }publicstaticvoidunitResolution(String[]pRules){Vectorrules = newVector();
 for(intri=0; ri<pRules.length; ri++)rules.add(rewrite(pRules[ri]));
 for(intri=0; ri<rules.size(); ri++){Stringrule1 = (String)rules.get(ri);
 if(rule1.indexOf(",")>0)continue; // it's not unit rule.Stringterm = rule1;
 StringnegTerm = neg(term);
 for(intrj=0; rj<rules.size(); rj++){Stringrule2 = (String)rules.get(rj);
 Stringexp = ","+rule2+",";
 if(exp.indexOf(","+negTerm+",")>0){StringunifyExp = replace(exp, ","+negTerm+",", ",");
 StringnewRule = unifyExp.substring(1, unifyExp.length()-1);
 rules.add(newRule);
 System.out.println("unfiy("+rule1+"|"+rule2+")="+newRule);
 }}}}publicstaticvoidhornReasoning(String[]rules){TreeMaptrueMap = newTreeMap();
 intsatisfyRuleCount;
 do{satisfyRuleCount = 0;
 for(intri=0; ri<rules.length; ri++){if(rules[ri].length() == 0)continue;
 Stringhead = head(rules[ri], "<-");
 Stringbody = tail(rules[ri], "<-");
 String[]conds = body.split(",");
 booleanisSatisfy = true;
 for(intci=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);
 }publicstaticStringhead(StringpStr, StringpSpliter){intspliterPos = pStr.indexOf(pSpliter);
 if(spliterPos < 0)returnpStr;
 returnpStr.substring(0,spliterPos);
 }publicstaticStringtail(StringpStr, StringpSpliter){intspliterPos = pStr.indexOf(pSpliter);
 if(spliterPos < 0)return"";
 returnpStr.substring(spliterPos+pSpliter.length());
 }publicstaticStringreplace(StringpStr, StringfromPat, StringtoPat){if(fromPat.length()==0)returnpStr;
 if(pStr.indexOf(fromPat)<0)returnpStr;
 StringBufferrzStr = newStringBuffer();
 intstrIdx = 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));
 returnrzStr.toString();
 }}