import java.util.*;

class BooleanLogic {
	Random random = new Random();
	
	public static void main(String[] args) {
		String rules = "a<-b,c;b<-d,e;c<-d,f;d;e;f";
		hornReasoning(rules.split(";"));
		unitResolution(rules.split(";"));
	}
	
	public static String neg(String pTerm) {
		if (pTerm.startsWith("-"))
			return pTerm.substring(1);
		else
			return "-"+pTerm;
	}
	
	public static String rewrite(String rule) {
		StringBuffer rzRule = new StringBuffer();
		String head = STR.head(rule, "<-");
		String body = STR.tail(rule, "<-");
		rzRule.append(head);
		if (body.length() > 0) {		
			String[] conds = body.split(",");
			for (int i=0; i<conds.length; i++)
				rzRule.append(","+neg(conds[i]));
		}
		return rzRule.toString();
	}
	
	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);
				}
			}
		}		
	}
	
	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);
	}
}

/* a-b(X),c(Y);b(X)<-d(X),e(X);c(Y)<-d(Y),f(Y);d(a);e(a);d(b);f(b) */