// $Id: Euler.java,v 1.27 2003/09/29 23:24:21 jderoo Exp $ // PxButton | build | javac -O *.java | import java.io.*; import java.net.*; import java.util.*; /** Euler proof mechanism. @author Jos De Roo */ public class Euler implements Serializable { Euler subj = null; // RDF subject String verb = null; // RDF predicate as absoluteized verb Euler obj = null; // RDF object String cverb = null; // compact verb int varid = -1; // variable id boolean bound = false; // variable binding state boolean vv = false; // variable verb state Euler ref = null; // to be dereferenced Euler premis = null; // to attach the premis Euler near = null; // to construct a conjunction Euler far = this; // to remember last clause Hashtable ns = null; // to table namespaces Hashtable nsp = null; // to table namespace prefixes Hashtable syn = null; // to table synonyms Hashtable dds = null; // to table log:definitiveDocument and Service properties int varmax = 0; // maximum variable count String baseURI = ""; // URI of base process Hashtable loaded = null; // to table document/engine pairs long engine = 1; // number of engines static final String version = "R3588"; static final String Elabel = "label"; static final String Etrace = "trace"; static final String IW = "') != null) return; String rk = fromWeb(uri); String u = baseURI; if (!uri.startsWith("data:")) loaded.put('<' + baseURI + '>', this); Vector vt = new Vector(); Parser np = new Parser(rk, vt, this, u); if (ns == null) { ns = new Hashtable(); nsp = new Hashtable(); syn = new Hashtable(); dds = new Hashtable(); ns.put("rdfs:", RDFS + "#>"); ns.put("log:", LOG + "#>"); ns.put("iw:", IW + "#>"); } StringBuffer gen = new StringBuffer("data:,"); if (debug || trace) System.err.println("load " + uri); while (true) { far.near = np.parse(); if (far.near == null) break; while (far.near != null) { if (far.near.verb.equals(LOGforAll)) { if (far.near.subj.subj == null && far.near.subj.obj == null) { if (!vt.contains(far.near.obj.verb)) vt.addElement(far.near.obj.verb); far.near = far.near.near; continue; } else { Euler fn = far.near; Vector wt = new Vector(); for (Enumeration e = vt.elements(); e.hasMoreElements(); wt.addElement(e.nextElement())); while (fn != null && fn.verb.equals(LOGforAll)) { if (!wt.contains(fn.obj.verb)) wt.addElement(fn.obj.verb); fn = fn.near; } if (wt.size() > varmax) varmax = wt.size(); far.near.subj.near = fn; far.near = far.near.subj; far.near.forX(false, wt); } } rewrite(true, far.near, np); if (far.near.verb.equals(LOGimplies)) { rewrite(false,far.near.subj, np); far.near.obj.premis = far.near.subj; if (far.near.obj.varid != -1) { Euler er = far.near.subj; while (er.verb.equals(RDFSfyi) || er.verb.equals("") || er.verb.equals(Etrace)) er = er.near; er.vv = true; } Euler fn = far.near; while (fn.obj.near != null) { fn.near = np.parse(false, LOGimplies); fn.near.subj = fn.subj; fn.near.obj = fn.obj.near; fn = fn.near; } } else if (far.near.verb.equals(OWLequivalentClass)) gen.append(far.near.subj + " " + RDFSsubClassOf + " " + far.near.obj + ". ") .append(far.near.obj + " " + RDFSsubClassOf + " " + far.near.subj + ". "); else if (far.near.verb.equals(OWLequivalentProperty)) gen.append(far.near.subj + " " + RDFSsubPropertyOf + " " + far.near.obj + ". ") .append(far.near.obj + " " + RDFSsubPropertyOf + " " + far.near.subj + ". "); else if (far.near.verb.startsWith(RDF + "#_")) gen.append(far.near.verb + " " + RDFSsubPropertyOf + " " + RDFSmember + ". "); else if (far.near.verb.equals(LOGdefinitiveDocument) || far.near.verb.equals(LOGdefinitiveService)) dds.put(far.near.subj.verb, far.near.obj.verb); if (debug || trace) System.err.println("@@ assert " + far.near); far = far.near; } } syno(this); String gener = gen.toString(); if (!gener.equals("data:,")) load(gener); if (vt.size() > varmax) varmax = vt.size(); doc++; } /** prepares that proof engine */ public synchronized void prepare() { boolean ot = think; long os = step; think = true; if (debug || trace) System.err.println("prepare " + baseURI); proof("data:,?s " + OWLsameAs + " ?o. "); step = os; think = ot; syno(this); } /** proofs a conjunction with that proof engine @param uri of the RDF resource @return proof */ public synchronized String proof(String uri) { root = this; if (loaded == null) loaded = new Hashtable(); String cj = fromWeb(uri); String u = baseURI; Vector vt = new Vector(); Parser np = new Parser(cj, vt, this, u); if (ns == null) { ns = new Hashtable(); nsp = new Hashtable(); syn = new Hashtable(); dds = new Hashtable(); ns.put("rdfs:", RDFS + "#>"); ns.put("log:", LOG + "#>"); ns.put("iw:", IW + "#>"); } StringBuffer gen = new StringBuffer("data:,"); Euler goal = new Euler(); Euler g = goal; if (debug || trace) System.err.println("proof " + uri); while (true) { g.near = np.parse(); if (g.near == null) break; while (g.near != null && g.near.verb != null) { rewrite(true, g.near, np); if (g.near.verb.equals(LOGforSome) || g.near.verb.equals(LOGforAll) || g.near.obj.verb != null && g.near.obj.verb.equals(LOGTruth)) { if (g.near.subj.subj == null && g.near.subj.obj == null) { if (g.near.obj != null && !vt.contains(g.near.obj.verb)) vt.addElement(g.near.obj.verb); } else { Euler fn = g.near; Vector wt = new Vector(); for (Enumeration e = vt.elements(); e.hasMoreElements(); wt.addElement(e.nextElement())); while (fn != null && (fn.verb.equals(LOGforSome) || fn.verb.equals(LOGforAll) || fn.obj.verb.equals(LOGTruth))) { if ((fn.verb.equals(LOGforSome) || fn.verb.equals(LOGforAll)) && !wt.contains(fn.obj.verb)) wt.addElement(fn.obj.verb); fn = fn.near; } if (wt.size() > varmax) varmax = wt.size(); g.near = g.near.subj; Euler gn = g; while (gn.near != null) { gn.near.forX(false, wt); gn = gn.near; } gn.near = fn; } g = g.near; } else { g.near.getX(false, vt); g.near.forX(false, vt); if (vt.size() > varmax) varmax = vt.size(); if (debug || trace) System.err.println("@@ query " + g.near); g = g.near; } if (g.subj.varid != -1 && // @@ comprehension (g.verb.equals(RDFtype) && g.obj.verb.equals(RDFList) || g.verb.equals(RDFfirst) || g.verb.equals(RDFrest) || g.verb.equals(RDFtype) && g.obj.verb.equals(OWLOntology) || g.verb.equals(RDFtype) && g.obj.verb.equals(OWLClass) || g.verb.equals(OWLintersectionOf) || g.verb.equals(OWLunionOf) || g.verb.equals(OWLcomplementOf) || g.verb.equals(OWLoneOf) || g.verb.equals(RDFtype) && g.obj.verb.equals(OWLRestriction) || g.verb.equals(OWLonProperty) || g.verb.equals(OWLallValuesFrom) || g.verb.equals(OWLsomeValuesFrom) || g.verb.equals(OWLhasValue) || g.verb.equals(OWLminCardinality) || g.verb.equals(OWLmaxCardinality) || g.verb.equals(OWLcardinality))) { if (g.verb.equals(RDFtype)) g.vv = true; gen.append(g); } } } reorder(goal); syno(goal); String gener = gen.toString(); if (!gener.equals("data:,")) load(gener); if (vt.size() > varmax) varmax = vt.size(); StringBuffer nsp = new StringBuffer(256); Enumeration en = ns.keys(); while (en.hasMoreElements()) { Object nsx = en.nextElement(); nsp.append("@prefix ").append(nsx).append(' ').append(ns.get(nsx)).append(".\n"); } nsp.append('\n'); int tab = 0; Euler[] vars = new Euler[varmax]; Euler lr = goal.near; Euler ts = null; Euler tsb = null; Euler ts1 = null; Euler ts2 = null; stack stack = new stack(); boolean not = false; long istep = step; StringBuffer proof = new StringBuffer(4096); proof.append("# Generated with http://www.agfa.com/w3c/euler/#").append(version); proof.append(" on ").append(new Date().toGMTString()).append("\n"); int pn = 0; if (!nope) { proof.append("{\n (\n"); Enumeration enu = loaded.keys(); while (enu.hasMoreElements()) proof.append(' ').append(enu.nextElement()).append('.').append(LOGsemantics).append('\n'); proof.append(" ).").append(LOGconjunction).append(" =>\n"); proof.append(" <").append(baseURI).append(">.").append(LOGsemantics).append("\n}\n"); pn = proof.length(); proof.append(WHYbecause).append("\n{\n"); } proof.append(nsp); int pns = proof.length(); proof.ensureCapacity(proof.length() * 2); StringBuffer pp = new StringBuffer(4096); StringBuffer pc = new StringBuffer(4096); StringBuffer pm = new StringBuffer(4096); Hashtable pct = new Hashtable(); Euler te = goal; while (te.near != null) { te.near = te.near.eval(false, vars, stack); te = te.near; } goal = goal.near; if (trace) System.err.println("[" + step + "]CALL: " + goal); long t = System.currentTimeMillis(); while (true) { if (goal == null) { t = System.currentTimeMillis() - t; if (proof.length() == pns) { if (!nope) { proof.setLength(pn); proof.append(WHYunknownBecause).append("\n{\n"); } proof.append("# No proof found for "); } else { Enumeration sen = syn.keys(); while (sen.hasMoreElements()) { Object sne = sen.nextElement(); if (sne.equals(syn.get(sne))) continue; proof.append(sne); proof.append(' '); proof.append(OWLsameAs); proof.append(' '); proof.append(syn.get(sne)); proof.append(".\n"); } proof.append("# Proof found for "); } proof.append(u); proof.append(" in ").append(step-istep).append(step-istep==1?" step":" steps"); proof.append(" (").append((long)((step-istep)*1000L/(t+0.01))).append(" steps/sec)"); proof.append(" using ").append(engine).append(engine==1?" engine":" engines"); if (!nope) proof.append("\n}.\n"); conc = pct; return proof.toString(); } not = false; try { if (goal.varid != -1 && goal.subj != null && goal.obj != null) { Euler gn = goal.eval(false, vars, stack); goal.verb = gn.verb; goal.cverb = gn.cverb; } if (goal.verb == null) { if (goal.obj.verb == OWLsameAs) synon(goal.obj); tab--; if (goal.obj.subj.varid != -1 || goal.obj.varid != -1 || goal.obj.obj.varid != -1) { pp.append('\n'); for (int i = tab; i >= 0; i--) pp.append(" "); goal.obj.whysubst(pp, tab); } if (pp.charAt(pp.length() - 2) == '.' && pp.charAt(pp.length() - 1) == ' ') pp.setCharAt(pp.length() - 2, '}'); else pp.append('}'); pp.append(" =>\n"); for (int i = tab; i > 0; i--) pp.append(" "); pp.append('{').append(goal.obj); if (pp.charAt(pp.length() - 2) == '.' && pp.charAt(pp.length() - 1) == ' ') pp.insert(pp.length() - 2, '}'); else pp.append("}. "); if (tab == 0) pc.append(goal.obj).append('\n'); } else if (goal.verb == "" && goal.subj.deref().bound) { // @@ single pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); pp.append(getLit(goal.subj)).append(". "); } else if (goal.verb == Etrace) System.err.println("[" + step + "] " + goal); else if (goal.verb == STRconcatenation) { Euler el = goal.subj.deref(); StringBuffer sb = new StringBuffer("\""); while (el.getFirst() != null) { sb.append(getLit(el.getFirst().deref())); el = el.getRest(); } sb.append("\""); Euler er = np.parse(sb.toString().intern()); if (goal.obj.unify(er, this, stack)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == STRequalIgnoringCase) { String sv = getLit(goal.subj.deref()); String ov = getLit(goal.obj.deref()); if (sv.toLowerCase().equals(ov.toLowerCase())) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == STRnotEqualIgnoringCase) { String sv = getLit(goal.subj.deref()); String ov = getLit(goal.obj.deref()); if (!sv.toLowerCase().equals(ov.toLowerCase())) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == STRgreaterThan) { String sv = getLit(goal.subj.deref()); String ov = getLit(goal.obj.deref()); if (sv.compareTo(ov) > 0) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == STRnotGreaterThan) { String sv = getLit(goal.subj.deref()); String ov = getLit(goal.obj.deref()); if (sv.compareTo(ov) <= 0) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == STRlessThan) { String sv = getLit(goal.subj.deref()); String ov = getLit(goal.obj.deref()); if (sv.compareTo(ov) < 0) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == STRnotLessThan) { String sv = getLit(goal.subj.deref()); String ov = getLit(goal.obj.deref()); if (sv.compareTo(ov) >= 0) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == STRstartsWith) { String sv = getLit(goal.subj.deref()); String ov = getLit(goal.obj.deref()); if (sv.startsWith(ov)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == STRendsWith) { String sv = getLit(goal.subj.deref()); String ov = getLit(goal.obj.deref()); if (sv.endsWith(ov)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == STRcontains) { String sv = getLit(goal.subj.deref()); String ov = getLit(goal.obj.deref()); if (sv.indexOf(ov) != -1) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == STRcontainsIgnoringCase) { String sv = getLit(goal.subj.deref()); String ov = getLit(goal.obj.deref()); if (sv.toLowerCase().indexOf(ov.toLowerCase()) != -1) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHsum) { Euler el = goal.subj.deref(); double d = 0; while (el.getFirst() != null) { d += new Double(getLit(el.getFirst().deref())).doubleValue(); el = el.getRest(); } StringBuffer sb = new StringBuffer().append(nat(goal.subj.deref(), d)); obj = np.parse(sb.toString().intern()); if (goal.obj.unify(obj, this, stack)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHdifference) { Euler el = goal.subj.deref(); double d = new Double(getLit(el.getFirst().deref())).doubleValue(); el = el.getRest(); while (el.getFirst() != null) { d -= new Double(getLit(el.getFirst().deref())).doubleValue(); el = el.getRest(); } StringBuffer sb = new StringBuffer().append(nat(goal.subj.deref(), d)); obj = np.parse(sb.toString().intern()); if (goal.obj.unify(obj, this, stack)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHproduct) { Euler el = goal.subj.deref(); double d = 1; while (el.getFirst() != null) { d *= new Double(getLit(el.getFirst().deref())).doubleValue(); el = el.getRest(); } StringBuffer sb = new StringBuffer().append(nat(goal.subj.deref(), d)); obj = np.parse(sb.toString().intern()); if (goal.obj.unify(obj, this, stack)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHquotient) { Euler el = goal.subj.deref(); double d = new Double(getLit(el.getFirst().deref())).doubleValue(); el = el.getRest(); while (el.getFirst() != null) { d /= new Double(getLit(el.getFirst().deref())).doubleValue(); el = el.getRest(); } StringBuffer sb = new StringBuffer().append(d); obj = np.parse(sb.toString().intern()); if (goal.obj.unify(obj, this, stack)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHintegerQuotient) { Euler el = goal.subj.deref(); double d = new Double(getLit(el.getFirst().deref())).doubleValue(); el = el.getRest(); while (el.getFirst() != null) { d /= new Double(getLit(el.getFirst().deref())).doubleValue(); el = el.getRest(); } StringBuffer sb = new StringBuffer().append(Integer.toString((int)d)); obj = np.parse(sb.toString().intern()); if (goal.obj.unify(obj, this, stack)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHremainder) { Euler el = goal.subj.deref(); double d = new Double(getLit(el.getFirst().deref())).doubleValue(); el = el.getRest(); while (el.getFirst() != null) { d %= new Double(getLit(el.getFirst().deref())).doubleValue(); el = el.getRest(); } StringBuffer sb = new StringBuffer().append(nat(goal.subj.deref(), d)); obj = np.parse(sb.toString().intern()); if (goal.obj.unify(obj, this, stack)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHnegation && goal.subj.bound) { double d = new Double(getLit(goal.subj.deref())).doubleValue(); StringBuffer sb = new StringBuffer().append(nat(goal.subj.deref(), -d)); obj = np.parse(sb.toString().intern()); if (goal.obj.unify(obj, this, stack)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHabsoluteValue) { double d = new Double(getLit(goal.subj.deref())).doubleValue(); StringBuffer sb = new StringBuffer().append(nat(goal.subj.deref(), d<0?-d:d)); obj = np.parse(sb.toString().intern()); if (goal.obj.unify(obj, this, stack)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHrounded) { double d = new Double(getLit(goal.subj.deref())).doubleValue(); StringBuffer sb = new StringBuffer().append(Math.round(d)); obj = np.parse(sb.toString().intern()); if (goal.obj.unify(obj, this, stack)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHexponentiation) { Euler el = goal.subj.deref(); double d = new Double(getLit(el.getFirst().deref())).doubleValue(); el = el.getRest(); while (el.getFirst() != null) { d = Math.pow(d, new Double(getLit(el.getFirst().deref())).doubleValue()); el = el.getRest(); } StringBuffer sb = new StringBuffer().append(nat(goal.subj.deref(), d)); obj = np.parse(sb.toString().intern()); if (goal.obj.unify(obj, this, stack)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHgreaterThan) { if (mathCompare(goal) > 0) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHnotGreaterThan) { if (mathCompare(goal) <= 0) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHlessThan) { if (mathCompare(goal) < 0) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHnotLessThan) { if (mathCompare(goal) >= 0) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHequalTo) { if (mathCompare(goal) == 0) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHnotEqualTo) { if (mathCompare(goal) != 0) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHmemberCount) { int n = 0; Euler el = goal.subj.deref(); while (el.getFirst() != null) { n++; el = el.getRest(); } StringBuffer sb = new StringBuffer().append(n); Euler er = np.parse(sb.toString().intern()); if (goal.obj.unify(er, this, stack)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == MATHproofCount) { boolean ot = think; think = true; String p = proof(toURI(goal.subj)); think = ot; StringBuffer sb = new StringBuffer().append(conc.size()); Euler er = np.parse(sb.toString().intern()); if (goal.obj.unify(er, this, stack)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == LOGequalTo) { if (goal.subj.deref().verb == goal.obj.deref().verb) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == LOGnotEqualTo) { if (goal.subj.deref().verb != goal.obj.deref().verb) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == LOGincludes) { Euler e = new Euler(); engine++; e.load(toURI(goal.subj.deref())); String p = e.proof(toURI(goal.obj.deref())); if (p.indexOf("# Proof found") != -1) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == LOGnotIncludes) { Euler e = new Euler(); engine++; e.load(toURI(goal.subj.deref())); String p = e.proof(toURI(goal.obj.deref())); if (p.indexOf("# Proof found") == -1) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == LOGsemantics) { Euler e = np.parse(false, "^^"); e.subj = goal.subj.deref().copy(); e.obj = np.parse(false, LOGsemantics); if (goal.obj.deref().unify(e, this, stack)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == LOGracine) { String gsv = goal.subj.deref().verb; Euler er = goal.subj.deref(); if (gsv.indexOf('#') != -1) er = np.parse((gsv.substring(0, gsv.indexOf('#')) + '>').intern()); if (goal.obj.deref().unify(er, this, stack)) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else not = true; } else if (goal.verb == LOGimplies && (goal.subj.subj == null || goal.subj.verb == "^^" || goal.subj.verb == ".")) { Euler e = new Euler(); engine++; boolean ot = think; Euler el = goal.subj.deref(); while (el.getFirst() != null) { if (el.getFirst().getFirst() != null) think = true; else e.load(toURI(el.getFirst().deref())); el = el.getRest(); } e.prepare(); if (!tr) { System.out.println( "@prefix r: .\n" + "@prefix xsd: .\n" + "@prefix : <#>.\n"); tr = true; } if (goal.obj.toString().indexOf("Manifest") == -1 && goal.subj.deref().getFirst() != null) System.out.print("[ r:test " + (goal.subj.getFirst().verb=="."?goal.subj.getFirst().subj:goal.subj.getFirst()) + ";" + " r:begins \"" + now() + "\"^^xsd:dateTime; r:ends \""); String p = e.proof(toURI(goal.obj.deref())); boolean pass = p.indexOf("# Proof found") != -1; if (pass) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); pp.append(p); if (tab == 0) pc.append(p).append('\n'); } if (goal.obj.toString().indexOf("Manifest") == -1 && goal.subj.deref().getFirst() != null) System.out.println(now() + "\"^^xsd:dateTime; r:system :euler; " + "a " + (pass?"r:PassingRun":"r:IncompleteRun") + ", r:TestRun]."); think = ot; } else if ((goal.verb == RDFSsubClassOf || goal.verb == RDFSsubPropertyOf || goal.verb == OWLequivalentClass || goal.verb == OWLequivalentProperty || goal.verb == OWLsameAs) && goal.subj.deref().obj == null && goal.obj.deref().obj == null && goal.subj.deref().bound && goal.obj.deref().bound && goal.subj.deref().verb == goal.obj.deref().verb) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else if (goal.verb == RDFSfyi || goal.verb == RDFtype && goal.obj.deref().verb == RDFSContainerMembershipProperty && goal.subj.deref().verb.startsWith(RDF + "#_") || goal.verb == RDFtype && goal.obj.deref().verb == RDFSLiteral && (goal.subj.deref().verb.startsWith("\"") || goal.subj.deref().verb == "^^" && goal.subj.deref().subj.deref().verb.startsWith("\"") || goal.subj.deref().isNumeral()) || goal.verb == RDFtype && goal.obj.deref().verb == XSDstring && goal.subj.deref().verb.startsWith("\"") && goal.subj.deref().verb.endsWith("\"") || goal.cverb.endsWith(Xrcsid + '>')) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } else { Euler gd = goal.deref(); boolean b = mstep == -1 || step-istep < mstep*engine; boolean d = dds.get(goal.verb) != null; if (ts == null) { lr = this.near; while (lr != null) { ts = lr; if (b && !gd.vv && ts.verb == LOGimplies && (ts.obj.verb == gd.verb || !ts.obj.bound && gd.bound) && (!d || ts.subj.subj.verb.indexOf("log-rules#log1d") != -1)) { ts = ts.obj; break; } if (b && !d && ts.verb == gd.verb) break; else lr = lr.near; ts = null; } } if (ts != null) { Euler n = lr.near; tsb = null; while (n != null) { tsb = n; if (b && !gd.vv && tsb.verb == LOGimplies && (tsb.obj.verb == gd.verb || !tsb.obj.bound && gd.bound) && (!d || tsb.subj.subj.verb.indexOf("log-rules#log1d") != -1)) { tsb = tsb.obj; break; } if (b && !d && tsb.verb == gd.verb) break; else n = n.near; tsb = null; } if (tsb != null) { stack.push(goal, 0); stack.push(tsb, 0); stack.push(n, 0); stack.push(null, pp.length()); stack.push(null, pc.length()); stack.push(null, tab); } int hc = ts.hashCode(); for (int i = 0; i < varmax; i++) vars[i] = null; if (ts.eval(false, vars, stack).unify(goal, this, stack)) { if (ts.varid != -1) { vars[ts.varid].verb = gd.verb; vars[ts.varid].cverb = gd.cverb; vars[ts.varid].varid = gd.varid; vars[ts.varid].bound = true; vars[ts.varid].vv = true; } Euler ep = goal.near; // @@ euler paths while (ep != null) { if (ep.verb == null && hc == ep.varid && ep.obj.unify(goal, this, null)) break; ep = ep.near; } if (ep != null) { if (trace) System.err.println("@@ cycle " + ep); not = true; } else { ts = ts.premis; if (ts != null) { ts2 = new Euler(); ts1 = ts2; while (ts != null) { ts1.near = ts.eval(false, vars, stack); ts1 = ts1.near; ts = ts.near; } ts1.near = new Euler(); ts1 = ts1.near; ts1.cverb = "[" + step + "]"; ts1.obj = goal; ts1.bound = true; ts1.varid = hc; ts1.near = goal.near; ts1.far = goal.far; goal = ts2; if (pp.length() > 1 && pp.charAt(pp.length() - 2) == '.' && pp.charAt(pp.length() - 1) == ' ') { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); } if (pp.length() == 0) pp.append(' '); else if (pp.length() > 0 && pp.charAt(pp.length() - 1) != '{') pp.append(' '); pp.append('{'); tab++; } else { if (goal.verb == OWLsameAs) synon(goal); if (pp.length() > 1 && pp.charAt(pp.length() - 2) == '.' && pp.charAt(pp.length() - 1) == ' ') { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(" "); } goal.whysub(pp, tab); if (tab == 0) pc.append(goal).append('\n'); } } } else not = true; } else not = true; } } catch (Throwable exc) { if (debug || trace) System.err.println(exc); not = true; } if (trace) { if (!not && goal.verb != null) System.err.println("[" + step + "]EXIT: " + goal); else if (!not && goal.cverb != null) System.err.println(goal.cverb + "EXIT: " + goal.obj); else if (not && goal.verb != null) System.err.println("[" + step + "]FAIL: " + goal); else if (not && goal.cverb != null) System.err.println(goal.cverb + "FAIL: " + goal.obj); } if (goal.verb != null) { step++; if (debug && step % 1000000 == 0) System.err.println(step + " steps for " + u); } goal = goal.near; if (trace && !not && goal != null && goal.verb != null) System.err.println("[" + step + "]CALL: " + goal); if (!not && goal == null) { if (pm.length() != 0) proof.append(pm); else if (nope) proof.append(pc); else proof.append(pp); proof.append("\n"); if (trace) System.err.println("@@ continue"); pct.put(pc.toString(), this); } if (not || think && goal == null) { goal = null; Euler b = null; while ((b = stack.pop()) != null) { if (b.bound) { b.bound = false; b.ref = null; } else { tab = b.varid; pc.setLength(stack.pop().varid); pp.setLength(stack.pop().varid); lr = stack.pop(); ts = stack.pop(); goal = stack.pop(); if (trace) System.err.println("[" + step + "]REDO: " + goal); break; } } } } } final Euler eval(boolean f, Euler[] v, stack s) { if (ref != null && obj == null) return ref.eval(f, v, s); if (bound && varid == -1 && obj == null) return this; if (varid != -1 && v[varid] == null) v[varid] = new Euler(); if (varid != -1 && v[varid] != null && v[varid].vv) { Euler t = new Euler(); if (subj != null) t.subj = subj.eval(true, v, s); if (obj != null) t.obj = obj.eval(true, v, s); t.verb = v[varid].verb; t.cverb = v[varid].cverb; t.varid = v[varid].varid; t.bound = true; return t; } else if (obj != null) { Euler t = new Euler(); if (subj != null) t.subj = subj.eval(true, v, s); if (obj != null) t.obj = obj.eval(true, v, s); t.verb = verb; t.cverb = cverb; t.varid = varid; if (v != null && !bound && varid != -1) { if (v[varid] != t) t.ref = v[varid]; t.bound = true; s.push(t, 0); } else t.bound = true; t.vv = vv; if (f && near != null) t.near = near.eval(true, v, s); else t.near = near; return t; } v[varid].verb = verb; v[varid].cverb = cverb; v[varid].varid = varid; return v[varid]; } final boolean unify(Euler t, Euler r, stack s) { if (t == null) return false; if (ref != null && obj == null) return ref.unify(t, r, s); if (t.ref != null && t.obj == null) return unify(t.ref, r, s); if (bound && t.bound) { if (obj != null && verb == "^^" && t.verb == "^^" && subj.bound && t.subj.bound && (obj.unify(t.obj, r, s) || Datatype.isNumeric(r.getType(this)) && Datatype.isNumeric(r.getType(t))) || (verb == "^^" && subj.bound && obj.bound && t.obj == null || obj == null && t.verb == "^^" && t.subj.bound && t.obj.bound) && (r.getType(this) == r.getType(t) || Datatype.isNumeric(r.getType(this)) && Datatype.isNumeric(r.getType(t)))) return Datatype.compare(r.getType(this), r.getLit(this), r.getType(t), r.getLit(t)) == 0; if (varid == -1 && verb != null && t.verb != null && deref().verb != t.deref().verb) return false; if (subj != null && !subj.unify(t.subj, r, s)) return false; if (obj != null && !obj.unify(t.obj, r, s)) return false; if (near != null && near.verb == RDFrest && t.near.verb == RDFrest && !near.unify(t.near, r, s)) return false; return true; } if (bound) return t.unify(this, r, s); if (s != null) { if (t.varid != -1 && t.varid != varid && t.oc(varid)) return false; if (subj != null && !subj.unify(t.subj, r, s)) return false; if (obj != null && !obj.unify(t.obj, r, s)) return false; if (near != null && near.verb == RDFrest && t.near.verb == RDFrest && !near.unify(t.near, r, s)) return false; if (t != deref()) deref().ref = t; bound = true; s.push(this, 0); } return true; } final boolean oc(int vi) { if (ref != null) return ref.oc(vi); if (bound) { if (subj != null && subj.oc(vi)) return true; if (obj != null && obj.oc(vi)) return true; return false; } else return (varid == vi); } final void rewrite(boolean eu, Euler el, Parser np) { if (el.subj != null && el.subj.cverb == null) el.subj.verb = el.subj.cverb = (eu?"_:":"?v") + el.subj.hashCode() + "_" + doc; if (el.obj != null && el.obj.cverb == null) el.obj.verb = el.obj.cverb = (eu?"_:":"?v") + el.obj.hashCode() + "_" + doc; if (eu && el.subj != null && el.subj.cverb.startsWith("?")) el.subj.verb = el.subj.cverb = "_:" + el.subj.cverb.substring(1) + "_" + doc; if (eu && el.obj != null && el.obj.cverb.startsWith("?")) el.obj.verb = el.obj.cverb = "_:" + el.obj.cverb.substring(1) + "_" + doc; if (el.subj != null && el.subj.subj == null && el.subj.obj != null && el.subj.getFirst() == null) { Euler gr = el.subj.copy(); Euler gv = np.parse(false, (eu?"_:":"?v") + gr.hashCode() + "_" + doc); el.subj = gv; Euler gl = gr; while (true) { gl.subj = gv; np.swap(gl); if (gl.near == null) break; gl = gl.near; } gl.near = el.near; el.near = gr; if (el.verb.equals("")) { el.subj = gr.subj; el.verb = gr.verb; el.obj = gr.obj; el.cverb = gr.cverb; el.varid = gr.varid; el.bound = gr.bound; el.near = gr.near; } } if (el.obj != null && el.obj.subj == null && el.obj.obj != null) { Euler gr = el.obj.copy(); Euler gv = np.parse(false, (eu?"_:":"?v") + gr.hashCode() + "_" + doc); el.obj = gv; Euler gl = gr; while (true) { gl.subj = gv; np.swap(gl); if (gl.near == null) break; gl = gl.near; } gl.near = el.near; el.near = gr; } if (el.subj != null && el.subj.verb == "^" && el.verb != LOGimplies) { Euler gr = el.subj.copy(); rewrite(eu, gr, np); Euler gv = np.parse(false, (eu?"_:":"?v") + gr.hashCode() + "_" + doc); el.subj = gv; Euler gl = gr; gl.verb = gl.obj.verb; gl.cverb = gl.obj.cverb; gl.varid = gl.obj.varid; gl.bound = gl.obj.bound; gl.obj = gl.subj.copy(); gl.subj = gv; np.swap(gl); while (gl.near != null) gl = gl.near; gl.near = el.near; el.near = gr; } if (el.obj != null && el.obj.verb == "^" && el.verb != LOGimplies) { Euler gr = el.obj.copy(); rewrite(eu, gr, np); Euler gv = np.parse(false, (eu?"_:":"?v") + gr.hashCode() + "_" + doc); el.obj = gv; Euler gl = gr; gl.verb = gl.obj.verb; gl.cverb = gl.obj.cverb; gl.varid = gl.obj.varid; gl.bound = gl.obj.bound; gl.obj = gl.subj.copy(); gl.subj = gv; np.swap(gl); while (gl.near != null) gl = gl.near; gl.near = el.near; el.near = gr; } if (el.subj != null && el.subj.verb == "." && el.verb != LOGimplies) { Euler gr = el.subj.copy(); rewrite(eu, gr, np); Euler gv = np.parse(false, (eu?"_:":"?v") + gr.hashCode() + "_" + doc); el.subj = gv; Euler gl = gr; gl.verb = gl.obj.verb; gl.cverb = gl.obj.cverb; gl.varid = gl.obj.varid; gl.bound = gl.obj.bound; gl.obj = gv; np.swap(gl); while (gl.near != null) gl = gl.near; gl.near = el.near; el.near = gr; } if (el.obj != null && el.obj.verb == "." && el.verb != LOGimplies) { Euler gr = el.obj.copy(); rewrite(eu, gr, np); Euler gv = np.parse(false, (eu?"_:":"?v") + gr.hashCode() + "_" + doc); el.obj = gv; Euler gl = gr; gl.verb = gl.obj.verb; gl.cverb = gl.obj.cverb; gl.varid = gl.obj.varid; gl.bound = gl.obj.bound; gl.obj = gv; np.swap(gl); while (gl.near != null) gl = gl.near; gl.near = el.near; el.near = gr; } } final Euler copy() { Euler el = new Euler(); if (subj != null) el.subj = subj.copy(); el.verb = verb; if (obj != null) el.obj = obj.copy(); el.cverb = cverb; el.varid = varid; el.bound = bound; if (ref != el) el.ref = ref; el.premis = premis; if (near != null) el.near = near.copy(); el.far = far; return el; } final void getX(boolean f, Vector wt) { if (subj != null) subj.getX(true, wt); if (verb != null && (verb.startsWith("_:") || verb.startsWith("?")) && !wt.contains(verb)) wt.addElement(verb); if (obj != null) obj.getX(true, wt); if (f && near != null) near.getX(f, wt); } final void forX(boolean f, Vector wt) { if (subj != null) subj.forX(true, wt); if (verb != null && wt.indexOf(verb) != -1) { varid = wt.indexOf(verb); bound = false; } if (obj != null) obj.forX(true, wt); if (f && near != null) near.forX(f, wt); } void reorder(Euler er) { Euler el = er.near; Euler elc = null, elcp = null, elv = null, elvp = null; while (el != null) { if (el.varid != -1 || el.verb.equals(RDFtype)) { if (elv == null) elvp = elv = el; else elvp = elvp.near = el; } else { if (elc == null) elcp = elc = el; else elcp = elcp.near = el; } el = el.near; } if (elvp != null) elvp.near = null; if (elcp != null) elcp.near = elv; if (elc != null) er.near = elc; } void synon(Euler t) { if (t.subj.deref().verb.equals("^^") || t.obj.deref().verb.equals("^^")) return; boolean w = !t.subj.deref().verb.startsWith(W3C); String s = w?t.subj.deref().verb:t.obj.deref().verb; String o = w?t.obj.deref().verb:t.subj.deref().verb; if (o == null || s == null) return; if (t.subj != null && t.obj != null && t.subj.subj == null && t.subj.obj == null && t.obj.subj == null && t.obj.obj == null) { if (!s.equals(o)) syn.put(s, o); for (Enumeration e = syn.keys(); e.hasMoreElements(); ) { String k = (String)e.nextElement(); if (syn.get(k).equals(s)) { if (!k.equals(o)) syn.put(k, o); else syn.remove(k); } } } else if (t.subj != null && t.obj == null && t.subj.subj == null && t.subj.obj == null) syn.put(s, t); else if (t.subj == null && t.obj != null && t.obj.subj == null && t.obj.obj == null) syn.put(o, t); } void syno(Euler t) { for (Euler el = t; el != null; el = el.near) synt(el); } void synt(Euler t) { if (t.subj != null) syno(t.subj); if (t.verb != null) { Object o = syn.get(t.verb); if (o != null) { if (o instanceof String) t.verb = (String)o; else t.verb = o.toString(); } t.verb = t.verb.intern(); } if (t.obj != null) syno(t.obj); } final Euler deref() { if (ref != null) return ref.deref(); else return this; } final String stringf(boolean f) { if (ref != null && obj == null) return ref.stringf(f); String cv = deref().cverb; if (cv != null && cv.equals("^^")) return subj + "^^" + obj; if (cv != null && cv.equals("^")) return subj + "^" + obj; if (cv != null && cv.equals(".")) { if (!root.getLit(deref()).equals(deref().verb)) return root.getLit(deref()); else return subj + "." + obj; } if (f && subj != null && subj.varid == -1 || obj == null) { if (cv == null) return deref().verb; return cv; } Euler el = deref(); Euler en = null; StringBuffer r = new StringBuffer(64); boolean sv = subj != null && subj.ref == null && subj.subj == null && subj.cverb != null && subj.cverb.equals("[]") && subj.obj == null; boolean ov = obj != null && obj.ref == null && obj.subj == null && obj.cverb != null && obj.cverb.equals("[]") && obj.obj == null; boolean b = verb != null && !verb.equals(LOGimplies) && !verb.equals(LOGincludes) && !verb.equals(LOGnotIncludes) && !verb.equals(LOGinconsistentWith) && !verb.equals(MATHproofCount) && !verb.equals(OWLsameAs); if (el.verb != null && el.verb.equals(RDFfirst) && el.subj == null && el.obj != null) { r.append("("); while (el != null && el.obj != null) { int i = r.length(); r.append(el.obj.deref().stringf(b && el.obj.subj != null && el.obj.obj != null)); if (r.length() > 1 && (r.charAt(r.length() - 2) == '.' && r.charAt(r.length() - 1) == ' ' || r.charAt(r.length() - 1) == ';')) { if (r.charAt(i) != ' ') { r.insert(i, '{'); r.setCharAt(r.length() - 2, '}'); } else { r.insert(i, '['); r.setCharAt(r.length() - 1, ']'); } } en = el.near.obj.deref(); if (en.verb.equals(RDFnil)) break; else if (!en.verb.equals(RDFfirst)) { r.append("/ "); r.append(en.stringf(b && en.subj != null && en.obj != null)); break; } r.append(' '); el = en; } r.append(')'); return r.toString(); } if (!sv && subj != null && verb != null && !b) { el = subj.deref(); while (el != null) { r.append(el.stringf(b && el.subj != null && el.obj != null)); el = el.near; } } else if (!sv && subj != null || !sv && subj != null && subj.deref().subj == null) { el = subj.deref(); r.append(el.stringf(b && el.subj != null && el.obj != null)); } if (r.length() > 1 && (r.charAt(r.length() - 2) == '.' && r.charAt(r.length() - 1) == ' ' || r.charAt(r.length() - 1) == ';')) { if (r.charAt(0) != ' ') { r.insert(0, '{'); r.setCharAt(r.length() - 2, '}'); } else { r.insert(0, '['); r.setCharAt(r.length() - 1, ']'); } } if (r.length() > 0 && r.charAt(r.length() - 1) != ' ') r.append(' '); r.append(debug?deref().verb:deref().cverb); r.append(' '); int i = r.length(); if (!ov && obj != null && verb != null && !b || !ov && obj != null && obj.deref().subj == null) { el = obj.deref(); while (el != null) { r.append(el.stringf(b && el.subj != null && el.obj != null)); el = el.near; } } else if (!ov && obj != null) r.append(obj.stringf(b && obj.subj != null && obj.obj != null)); if (r.length() > 1 && (r.charAt(r.length() - 2) == '.' && r.charAt(r.length() - 1) == ' ' || r.charAt(r.length() - 1) == ';')) { if (r.charAt(i) != ' ') { r.insert(i, '{'); r.setCharAt(r.length() - 2, '}'); } else { r.insert(i, '['); r.setCharAt(r.length() - 1, ']'); } } if (!sv && subj != null && r.charAt(r.length() - 1) == ' ') r.insert(r.length() - 1, '.'); else if (!sv && subj != null && r.charAt(r.length() - 1) != ' ') r.append(". "); else { r.append(';'); el = near; while (el != null) { r.append(' ').append(debug?el.deref().verb:el.deref().cverb).append(' '); r.append(el.obj.stringf(b && el.subj != null && el.obj != null)); r.append(';'); el = el.near; } r.insert(0, '['); r.setCharAt(r.length() - 1, ']'); } return r.toString(); } /** string represention of this Euler obj @return string */ public final String toString() { return stringf(false); } final Euler getFirst() { Euler er = this; if (verb == "^^" || verb == "^" || verb == ".") er = subj; while (er != null) { if (er.verb == RDFfirst) return er.obj; else er = er.near; } return null; } final Euler getRest() { Euler er = this; if (verb == "^^" || verb == "^" || verb == ".") er = subj; while (er != null) { if (er.verb == RDFrest) return er.obj; else er = er.near; } return null; } final String getLit(Euler el) { String s = el.verb; if (s == "." && el.obj.verb.startsWith(MATH)) { proof("data:," + el.subj + " " + el.obj + " ?x. "); if (obj != null) s = obj.cverb; } if (s == "^^") return getLit(el.subj.deref()); if (s.startsWith("\"\"\"")) return s.substring(3, s.length() - 3); if (s.indexOf('"') != -1) return s.substring(s.indexOf('"') + 1, s.lastIndexOf('"')); return s; } final String getType(Euler el) { if (el.obj == null) { if (el.isNumeral()) return XSDdouble; else return XSDstring; } else return el.obj.deref().verb; } final double mathCompare(Euler el) { Euler s = el.subj.deref(); Euler o = el.obj.deref(); if ((s.verb == "^^" || o.verb == "^^") && (getType(s) == getType(o) || Datatype.isNumeric(getType(s)) && Datatype.isNumeric(getType(o)))) return Datatype.compare(getType(s), getLit(s), getType(o), getLit(o)); return new Double(getLit(s)).doubleValue() - new Double(getLit(o)).doubleValue(); } final void whysub(StringBuffer sb, int tab) { if (subj.varid != -1 || varid != -1 || obj.varid != -1) { sb.append(" {"); whysubst(sb, tab); sb.append("} =>\n"); for (int i = tab; i > 0; i--) sb.append(" "); sb.append("{").append(this); if (sb.charAt(sb.length() - 2) == '.' && sb.charAt(sb.length() - 1) == ' ') sb.insert(sb.length() - 2, '}'); else sb.append("}. "); } else sb.append(this); } final void whysubst(StringBuffer sb, int tab) { Parser np = new Parser(); Euler el = np.parse(false, "="); el.subj = np.parse(false, IWV); if (subj.varid != -1) { el.subj.obj = np.parse(false, "\"" + subj.cf() + "\""); el.obj = subj.deref(); sb.append(el).append('\n'); for (int i = tab; i >= 0; i--) sb.append(" "); } if (varid != -1) { sb.append("[").append(IWV).append(" \"").append(cf()).append("\"] = ").append(deref().cverb).append(".\n"); for (int i = tab; i >= 0; i--) sb.append(" "); } if (obj.varid != -1) { el.subj.obj = np.parse(false, "\"" + obj.cf() + "\""); el.obj = obj.deref(); sb.append(el).append('\n'); for (int i = tab; i >= 0; i--) sb.append(" "); } if (subj.varid != -1) sb.append("[").append(IWV).append(" \"").append(subj.cf()).append("\"] "); else sb.append(subj.cf()).append(" "); if (varid != -1) sb.append("[").append(IWV).append(" \"").append(cf()).append("\"] "); else sb.append(cf()).append(" "); if (obj.varid != -1) sb.append("[").append(IWV).append(" \"").append(obj.cf()).append("\"]"); else sb.append(obj.cf()); } final String cf() { if (subj == null && verb == RDFfirst) return this.toString(); if (cverb == "^^") return subj + "^^" + obj; else return cverb; } final String fromWeb(String uri) { StringBuffer sb = new StringBuffer(); String rl = null; if (uri.startsWith("data:")) { baseURI = ""; return uri.substring(uri.indexOf(',') + 1); } else if (uri.startsWith("http:")) { try { baseURI = uri.startsWith("http://localhost/AskJena?fromWeb=")?"http://"+uri.substring(34):uri; if (!local || uri.startsWith("http://localhost")) { URL r = new URL(uri); String p = r.getPath(); String hp = System.getProperty("http_proxy"); if (hp != null && !hp.equals("") && !hp.equals("%http_proxy%") && !uri.startsWith("http://localhost")) { r = new URL(hp); p = uri; } Socket so = new Socket(r.getHost(), r.getPort()==-1?80:r.getPort()); so.setTcpNoDelay(true); DataOutputStream dos = new DataOutputStream(new BufferedOutputStream(so.getOutputStream())); DataInputStream dis = new DataInputStream(new BufferedInputStream(so.getInputStream())); PrintWriter pw = new PrintWriter(new OutputStreamWriter(dos, "UTF8"), true); pw.println("GET " + p + " HTTP/1.0"); pw.println("Host: " + r.getHost()); pw.println(""); pw.flush(); BufferedReader br = new BufferedReader(new InputStreamReader(dis, "UTF8")); if ((rl = br.readLine()).indexOf("200") == -1) throw new RuntimeException(rl); while (!br.readLine().equals("")); while ((rl = br.readLine()) != null) { sb.append(rl); sb.append('\n'); } dis.close(); dos.close(); so.close(); } else { FileInputStream fis = new FileInputStream(uri.substring(6)); DataInputStream dis = new DataInputStream(new BufferedInputStream(fis)); BufferedReader br = new BufferedReader(new InputStreamReader(dis, "UTF8")); while ((rl = br.readLine()) != null) { sb.append(rl); sb.append('\n'); } dis.close(); fis.close(); } } catch (Exception e) { return AskJena.fromWeb(!local?uri:uri.substring(6)); } } else { String file = uri; if (file.startsWith("file:")) file = file.substring(file.lastIndexOf(':') + 1); if (file.indexOf('#') != -1) file = file.substring(0, file.lastIndexOf('#')); try { String path = System.getProperty("user.dir").replace(File.separatorChar, '/'); path = path.substring(path.indexOf('/')) + "/"; baseURI = "file:" + ((file.charAt(0) == '/' || file.charAt(1) == ':')?"":path) + file; FileInputStream fis = new FileInputStream(file); DataInputStream dis = new DataInputStream(new BufferedInputStream(fis)); BufferedReader br = new BufferedReader(new InputStreamReader(dis, "UTF8")); while ((rl = br.readLine()) != null) { sb.append(rl); sb.append('\n'); } dis.close(); fis.close(); } catch (Exception e) { return AskJena.fromWeb(uri); } } return sb.toString(); } final String toURI(Euler el) { if (el.verb == "^^" || el.verb == "^" || el.verb == ".") el = el.subj; if (el.obj != null) { StringBuffer sb = new StringBuffer("data:,"); for (Enumeration en = ns.keys(); en.hasMoreElements(); ) { Object nsx = en.nextElement(); sb.append("@prefix ").append(nsx).append(' ').append(ns.get(nsx)).append(".\n"); } for (Euler eu = el; eu != null; eu = eu.near) sb.append(eu); return sb.toString(); } else if (el.verb.equals("this")) return baseURI; else if (el.verb.startsWith(RDF)) return "http://www.agfa.com/w3c/euler/rdf-rules.n3"; else if (el.verb.startsWith(RDFS)) return "http://www.agfa.com/w3c/euler/rdfs-rules.n3"; else if (el.verb.startsWith(XSD)) return "http://www.agfa.com/w3c/euler/xsd-rules.n3"; else if (el.verb.startsWith(OWL)) return "http://www.agfa.com/w3c/euler/owl-rules.n3"; else { String s = el.verb; if (s.charAt(0) == '<') s = s.substring(1, s.length() - 1); if (s.charAt(s.length() - 1) == '#') s = s.substring(0, s.length() - 1); if (s.endsWith(".rdf")) s = s.substring(0, s.length() - 4) + ".n3"; else if (!s.endsWith(".n3") && !s.endsWith(".nt")) s = s + ".n3"; return s; } } final String nat(Euler el, double d) { if (el.getFirst() == null && getLit(el.deref()).indexOf('.') != -1) return Double.toString(d); while (el.getFirst() != null) { if (getLit(el.getFirst().deref()).indexOf('.') != -1) return Double.toString(d); el = el.getRest(); } return Integer.toString((int)d); } final boolean isNumeral() { try { new Double(verb); return true; } catch (Throwable t) { return false; } } final String now() { String t = new Date().toGMTString(); Date d = new Date(t.substring(0, t.length() - 4)); StringBuffer sb = new StringBuffer(); sb.append(d.getYear() + 1900).append('-') .append(d.getMonth()<9?"0":"").append(d.getMonth() + 1).append('-') .append(d.getDate()<10?"0":"").append(d.getDate()).append('T') .append(d.getHours()<10?"0":"").append(d.getHours()).append(':') .append(d.getMinutes()<10?"0":"").append(d.getMinutes()).append(':') .append(d.getSeconds()<10?"0":"").append(d.getSeconds()).append('Z'); return sb.toString(); } final String toHex(String s) { StringBuffer sb = new StringBuffer(); for (int i = 0; i < s.length(); i++) sb.append(Integer.toHexString(s.charAt(i))); return sb.toString(); } /** Main method invoked via java Euler @param args [--think] [--nope] [--step count] [--debug] [--trace] axiom ... lemma */ public static void main(String[] args) { if (args.length == 0) System.err.println("java [-Dhttp_proxy=%http_proxy%] Euler [--think] [--nope] [--step count] [--debug] [--trace] axiom ... lemma"); else { try { step = 1; trace = false; think = false; PrintStream out = System.out; Euler e = new Euler(); Parser np = new Parser(); int n = args.length - 1; if (args[n].startsWith(">")) { out = new PrintStream(new FileOutputStream(new File(args[n].substring(1)))); n--; } for (int j = 0; j < n; j++) { if (args[j].endsWith("-think")) think = true; else if (args[j].endsWith("-nope")) nope = true; else if (args[j].endsWith("-step")) mstep = Long.parseLong(args[++j]); else if (args[j].endsWith("-local")) local = true; else if (args[j].endsWith("-debug")) debug = true; else if (args[j].endsWith("-trace")) trace = true; else if (!args[j].startsWith("-")) e.load(e.toURI(np.parse('<' + args[j] + '>'))); } e.prepare(); out.println(e.proof(e.toURI(np.parse('<' + args[n] + '>')))); if (out != System.out) out.close(); } catch (Exception e) { e.printStackTrace(); } } } }