// $Id: Euler.java,v 1.338 2005/03/06 19:47:08 amdus Exp $ // PxButton | build | javac *.java | import java.net.URL; import java.net.Socket; import java.util.Date; import java.util.Vector; import java.util.Hashtable; import java.util.Enumeration; import java.io.File; import java.io.FileOutputStream; import java.io.PrintStream; import java.io.PrintWriter; import java.io.Serializable; import java.io.BufferedReader; import java.io.FileInputStream; import java.io.DataInputStream; import java.io.DataOutputStream; import java.io.InputStreamReader; import java.io.OutputStreamWriter; import java.io.BufferedInputStream; import java.io.BufferedOutputStream; /** * Euler proof mechanism. * * @author Jos De Roo */ public class Euler { 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 near = null; // to construct a conjunction Euler premis = null; // to attach the premis Euler ref = null; // to be dereferenced Euler far = this; // to remember last clause long uid = uidc++; // unique id String src = null; // triple source int line = -1; // triple source line EulerExt ext = null; // extensions static final String E = "')) return; String rk = fromWeb(uri); String u = ext.baseURI; if (!uri.startsWith("data:")) ext.loaded.addElement('<' + ext.baseURI + '>'); if (!docv.contains(ext.baseURI)) docv.addElement(ext.baseURI); doc = docv.indexOf(ext.baseURI); Vector vt = new Vector(); Parser np = new Parser(rk, vt, this, u); StringBuffer gen = new StringBuffer("data:,"); if (Outputter.log) Outputter.getInstance().log("Euler", "load", "engine" + uid + " load " + uri, ILogger.FINE); while (true) { far.near = np.parse(); if (far.near == null) break; while (far.near != null && far.near.verb != 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() > ext.varmax) ext.varmax = wt.size(); far.near.subj.near = fn; far.near = far.near.subj; far.near.forX(false, wt); } } far.near.forX(false, vt); rewrite(true, far.near, np); if (uid != -1 && far.near.verb.equals(Qselect) && far.near.near.verb.equals(Qwhere)) { far.near.obj.src = far.near.subj.verb; far.near.subj = far.near.near.obj; far.near.verb = LOGimplies; far.near.cverb = "=>"; far.near.near = far.near.near.near; } if (far.near.verb.equals(LOGimplies) && far.near.subj.cverb.equals("{}")) far.near = far.near.obj; else if (far.near.verb.equals(LOGimplies) || far.near.verb.equals(LOGnotImplies)) { Euler fn = far.near.subj; while (fn != null) { if (fn.verb.equals(LOGincludes) && fn.toString().lastIndexOf('?') > fn.toString().indexOf("includes") && !far.near.subj.verb.equals(LOGdefinitiveDocument) && !far.near.subj.verb.equals(LOGdefinitiveService)) { rewrite(false, fn.obj, np); Euler oe = far.near.subj; far.near.subj = fn.obj.copy(); Euler ne = far.near.subj; while (ne.near != null) ne = ne.near; ne.near = oe; } else if (fn.subj.subj != null && fn.verb != "vv" && fn.subj.verb != "^^") rewrite(true, fn.subj, np); else if (fn.obj.subj != null && fn.verb != "vv" && fn.obj.verb != "^^") rewrite(true, fn.obj, np); fn = fn.near; } reorderPremis(far.near); rewrite(false, far.near.subj, np); far.near.obj.premis = far.near.subj; fn = far.near; while (fn.obj.near != null) { fn.near = np.parse(false, far.near.cverb); fn.near.subj = fn.subj; fn.near.obj = fn.obj.near; fn = fn.near; } fn = far.near.copy(); fn.near = fn.subj; fn.subj = fn.obj; fn.obj = fn.near; far.near.obj.near = null; } else if (far.near.verb.equals(OWLequivalentClass)) gen.append(far.near.subj).append(' ').append(RDFSsubClassOf).append(' ').append(far.near.obj).append(". ") .append(far.near.obj).append(' ').append(RDFSsubClassOf).append(' ').append(far.near.subj).append(". "); else if (far.near.verb.equals(OWLequivalentProperty)) gen.append(far.near.subj).append(' ').append(RDFSsubPropertyOf).append(' ').append(far.near.obj).append(". ") .append(far.near.obj).append(' ').append(RDFSsubPropertyOf).append(' ').append(far.near.subj).append(". "); else if (far.near.verb.startsWith(RDF + "#_")) gen.append(far.near.verb).append(' ').append(RDFSsubPropertyOf).append(' ').append(RDFSmember).append(". "); else if (far.near.verb.equals(RDFtype) && far.near.obj.verb.equals(RDFSClass)) ext.ocl.put(far.near.subj.verb, this); else if (far.near.verb.equals(RDFtype) && far.near.obj.verb.equals(OWLClass)) ext.ocl.put(far.near.subj.verb, this); else if (far.near.verb.equals(LOGdefinitiveDocument) || far.near.verb.equals(LOGdefinitiveService)) ext.dds.put(far.near.subj.verb, far.near.obj.verb); if (Outputter.log) Outputter.getInstance().log("Euler", "load", "engine" + uid + " assert " + far.near, ILogger.FINE); far = far.near; if (!ext.baseURI.startsWith("_:")) triple++; } } String gener = gen.toString(); String ob = ext.baseURI; if (!ext.se && !gener.equals("data:,")) load(gener); ext.baseURI = ob; if (vt.size() > ext.varmax) ext.varmax = vt.size(); } /** * prepares that proof engine */ public synchronized void prepare() { boolean ot = Configuration.getInstance().getThink(); long os = step; long op = triple; long om = Configuration.getInstance().getSteps(); if (Configuration.getInstance().getSteps() != -1) Configuration.getInstance().setSteps(Configuration.getInstance().getSteps()/20); Configuration.getInstance().setThink(true); if (Outputter.log) Outputter.getInstance().log("Euler", "prepare", "engine" + uid + " prepare " + ext.baseURI, ILogger.FINE); proof("data:,?S " + OWLsameAs + " ?O. "); Configuration.getInstance().setSteps(om); triple = op; step = os; Configuration.getInstance().setThink(ot); syno(this); } /** * proofs a conjunction with that proof engine * * @param uri uri of the RDF resource * * @return the proof */ public synchronized String proof(String uri) { root = this; if (ext == null) ext = new EulerExt(); if (ext.loaded == null) ext.loaded = new Vector(); String cj = fromWeb(uri); String u = ext.baseURI; Vector vt = new Vector(); Parser np = new Parser(cj, vt, this, u); StringBuffer gen = new StringBuffer("data:,"); Euler goal = new Euler(); Euler g = goal; if (Outputter.log) Outputter.getInstance().log("Euler", "proof", "engine" + uid + " proof " + uri, ILogger.FINE); 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.subj.subj != null && g.near.verb != "vv" && g.near.subj.verb != "^^") rewrite(true, g.near.subj, np); if (g.near.obj.subj != null && g.near.verb != "vv" && g.near.obj.verb != "^^") rewrite(true, g.near.obj, np); if (g.near.verb.equals(LOGimplies) && g.near.subj.cverb.equals("{}")) g.near = g.near.obj; if (g.near.verb.equals(Eevidence)) g.near = g.near.subj; 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); g.near = g.near.near; continue; } 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() > ext.varmax) ext.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 if (g.near.verb.endsWith(Xrcsid + '>')) { g.near = g.near.near; continue; } else { g.near.getX(false, vt); g.near.forX(false, vt); if (vt.size() > ext.varmax) ext.varmax = vt.size(); if (Outputter.log) Outputter.getInstance().log("Euler", "proof", "engine" + uid + " query " + g.near, ILogger.FINE); 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(OWLClass) || g.verb.equals(OWLintersectionOf) || g.verb.equals(OWLunionOf) || g.verb.equals(OWLcomplementOf) && (g.obj.varid != -1 || ext.ocl.get(g.obj.verb) != null) || 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); } } } if (goal.near == null) goal.near = np.parse(false, "{}"); if (Configuration.getInstance().getProofExplanation()) reorder(goal); syno(goal); String gener = gen.toString(); String ob = ext.baseURI; if (!ext.se && !gener.equals("data:,")) load(gener); ext.baseURI = ob; if (vt.size() > ext.varmax) ext.varmax = vt.size(); StringBuffer nsp = new StringBuffer(256); Enumeration en = ext.ns.keys(); while (en.hasMoreElements()) { Object nsx = en.nextElement(); nsp.append("@prefix ").append(nsx).append(' ').append(ext.ns.get(nsx)).append(".\n"); } nsp.append('\n'); int tab = 0; Euler[] vars = new Euler[ext.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); int pn = 0; if (!(ext.baseURI.startsWith("file:") && ext.baseURI.endsWith("test.n3"))) { proof.append("# Generated with http://www.agfa.com/w3c/euler/ version ").append(Configuration.getInstance().getVersion()); proof.append(" on ").append(new Date().toGMTString()).append("\n"); if (Configuration.getInstance().getProofExplanation()) { proof.append("@prefix log: .\n\n("); Enumeration enu = ext.loaded.elements(); while (enu.hasMoreElements()) { if (proof.charAt(proof.length() - 1) != '(') proof.append("\n "); proof.append(enu.nextElement()).append("!log:semantics"); } proof.append(")!log:conjunction =>\n{\n"); pn = proof.length(); } proof.append(nsp); } int pns = proof.length(); proof.ensureCapacity(proof.length() * 2); StringBuffer pp = new StringBuffer(4096); StringBuffer pc = 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 (Outputter.log) Outputter.getInstance().log("Euler", "proof", "engine" + uid + " [" + step + "]CALL: " + goal, ILogger.FINER); long t = System.currentTimeMillis(); while (true) { if (goal == null) { t = System.currentTimeMillis() - t; if (!(ext.baseURI.startsWith("file:") && ext.baseURI.endsWith("test.n3"))) { if (proof.length() == pns) { if (Configuration.getInstance().getProofExplanation()) proof.setLength(pn); proof.append("# No proof found for "); } else 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(ext.engine).append(ext.engine==1?" engine":" engines"); proof.append(" (").append(triple).append(triple==1?" triple)":" triples)"); if (!ext.baseURI.startsWith("_:")) triple = 0; if (Configuration.getInstance().getProofExplanation()) 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 && goal.obj.subj == null) { if (goal.obj.verb == OWLsameAs) synon(goal.obj); 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(goal.obj).append(" e:evidence ").append(goal.obj.src).append("}. "); if (tab == 0) { if (pct.get(goal.obj.toString()+'\n') == null) pc.append(goal.obj).append('\n'); else not = true; } } else if (goal.verb == null && goal.obj.subj.deref().bound && goal.obj.obj.deref().bound) { if (goal.obj.verb == OWLsameAs) synon(goal.obj); 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).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, goal.obj.src); if (pp.charAt(pp.length() - 2) == '.' && pp.charAt(pp.length() - 1) == ' ') pp.insert(pp.length() - 2, '}'); else pp.append("}. "); if (tab == 0) { if (pct.get(goal.obj.toString()+'\n') == null) pc.append(goal.obj).append('\n'); else not = true; } } else if (goal.verb == "" && goal.subj.deref().bound && goal.subj.deref().getFirst() == null) { // @@ 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 (!ext.se && goal.verb != null && BuiltinManager.getInstance().isBuiltin(goal.verb)) { not = BuiltinManager.getInstance().applyBuiltin(this, goal, stack, tab, pp, pc); } else if ((goal.verb == RDFSsubClassOf || goal.verb == RDFSsubPropertyOf || goal.verb == OWLequivalentClass || goal.verb == OWLequivalentProperty || goal.verb == OWLsameAs) && goal.subj.deref().verb == goal.obj.deref().verb && goal.subj.deref().obj == null && goal.obj.deref().obj == null && (goal.subj.deref().bound || goal.verb != OWLsameAs && goal.subj.deref().verb.startsWith("_:")) && (goal.obj.deref().bound || goal.verb != OWLsameAs && goal.obj.deref().verb.startsWith("_:"))) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(' '); pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, OWLkb); if (tab == 0) pc.append(goal).append('\n'); } else if (!ext.se && goal.verb == RDFtype && (goal.obj.deref().verb == RDFSResource || goal.obj.deref().verb == OWLThing || goal.obj.deref().verb == RDFSContainerMembershipProperty && goal.subj.deref().verb.startsWith(RDF + "#_") || goal.obj.deref().verb == RDFSLiteral && (goal.subj.deref().verb.startsWith("\"") || goal.subj.deref().verb == "^^" && goal.subj.deref().subj.deref().verb.startsWith("\"") && !Datatype.clash(goal.subj.deref().obj.verb, goal.subj.deref().subj.verb) || goal.subj.deref().isNumeral()) || goal.obj.deref().verb == XSDstring && goal.subj.deref().verb.startsWith("\"") && goal.subj.deref().verb.endsWith("\"") || goal.subj.deref().verb == "^^" && goal.subj.deref().obj.verb == goal.obj.deref().verb && !Datatype.clash(goal.subj.deref().obj.verb, goal.subj.deref().subj.verb))) { pp.append('\n'); for (int i = tab; i > 0; i--) pp.append(' '); pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, OWLkb); if (tab == 0) pc.append(goal).append('\n'); } else { Euler gd = goal.deref(); if (goal.varid != -1 && goal.subj == null && goal.obj == null) { Euler gn = goal.near; Euler gx = gd; while (gx.near != null) gx = gx.near; gx.near = gn; goal.near = gd.near; } boolean b = Configuration.getInstance().getSteps() == -1 || step-istep < Configuration.getInstance().getSteps()*ext.engine; String d = null; if (goal.verb != null) d = (String)ext.dds.get(goal.verb); 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 == null || d == ts.src)) { ts = ts.obj; break; } if (b && (d == null || d == ts.src) && gd.verb == "vv" && (ts.subj.obj == null || ts.subj.verb == "^^") && (ts.obj.obj == null || ts.obj.verb == "^^")) { ts = ts.cvv(); break; } if (b && (d == null || d == ts.src) && ts.verb == gd.verb) { if (gd.subj != null && gd.subj.verb == "vv" && gd.subj.subj != null) { Euler er = ts.copy(); er.subj = ts.subj.cvv(); ts = er; } if (gd.obj != null && gd.obj.verb == "vv" && gd.obj.subj != null) { Euler er = ts.copy(); er.obj = ts.obj.cvv(); ts = er; } 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 == null || d == tsb.src)) { tsb = tsb.obj; break; } if (b && (d == null || d == tsb.src) && gd.verb == "vv" && (tsb.subj.obj == null || tsb.subj.verb == "^^") && (tsb.obj.obj == null || tsb.obj.verb == "^^")) { tsb = tsb.cvv(); break; } if (b && (d == null || d == tsb.src) && tsb.verb == gd.verb) { if (gd.subj != null && gd.subj.verb == "vv" && gd.subj.subj != null) { Euler er = tsb.copy(); er.subj = tsb.subj.cvv(); tsb = er; } if (gd.obj != null && gd.obj.verb == "vv" && gd.obj.subj != null) { Euler er = tsb.copy(); er.obj = tsb.obj.cvv(); tsb = er; } 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); } long hc = ts.uid; for (int i = 0; i < ext.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.uid && ep.obj.unify(goal, this, null)) break; ep = ep.near; } if (ep != null) { if (Outputter.log) Outputter.getInstance().log("Euler", "proof", "engine" + uid + " cycle " + ep, ILogger.FINER); not = true; } else { String src = ts.src; if (src == null && ext.baseURI.startsWith("_:")) src = ext.baseURI; else if (src == null && !ext.baseURI.startsWith("_:")) src = '<' + ext.baseURI + '>'; else if (!src.startsWith("_:") && src.indexOf('#') == -1) src = src.substring(0, src.length() - 1)+ "#_" + ts.line + '>'; goal.src = src; 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.uid = 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(' '); } 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(' '); } pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, src); if (tab == 0) pc.append(goal).append('\n'); } } } else not = true; } else not = true; } } catch (NumberFormatException exc) { not = true; } catch (Throwable exc) { exc.printStackTrace(); not = true; } if (Outputter.log) { if (!not && goal.verb != null) Outputter.getInstance().log("Euler", "proof", "engine" + uid + " [" + step + "]EXIT: " + goal, ILogger.FINER); else if (!not && goal.cverb != null) Outputter.getInstance().log("Euler", "proof", "engine" + uid + " " + goal.cverb + "EXIT: " + goal.obj, ILogger.FINER); else if (not && goal.verb != null) Outputter.getInstance().log("Euler", "proof", "engine" + uid + " [" + step + "]FAIL: " + goal, ILogger.FINER); else if (not && goal.cverb != null) Outputter.getInstance().log("Euler", "proof", "engine" + uid + " " + goal.cverb + "FAIL: " + goal.obj, ILogger.FINER); } if (goal.verb != null) { step++; if (Outputter.log && step % 1000000 == 0) Outputter.getInstance().log("Euler", "proof", "engine" + uid + " " + step + " steps for " + u, ILogger.FINE); } goal = goal.near; if (Outputter.log && !not && goal != null && goal.verb != null) Outputter.getInstance().log("Euler", "proof", "engine" + uid + " [" + step + "]CALL: " + goal, ILogger.FINER); if (!not && goal == null) { if (!Configuration.getInstance().getProofExplanation()) proof.append(pc).append("\n"); else proof.append(pp).append("\n\n"); if (Outputter.log) Outputter.getInstance().log("Euler", "proof", "engine" + uid + " continue", ILogger.FINER); pct.put(pc.toString(), this); } if (not || Configuration.getInstance().getThink() && 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 (Outputter.log) Outputter.getInstance().log("Euler", "proof", "engine" + uid + " [" + step + "]REDO: " + goal, ILogger.FINER); 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 && (subj.unify(t.subj, r, s) && obj.unify(t.obj, r, s) || 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 != null && t.subj.bound && t.obj != null && t.obj.bound) && (r.getType(this) == r.getType(t) || Datatype.isNumeric(r.getType(this)) && Datatype.isNumeric(r.getType(t)) || Datatype.isAlphaNumeric(r.getType(this)) && Datatype.isAlphaNumeric(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 (subj == null && near != null && !near.unify(t.near, r, s)) return false; return true; } if (bound) return t.unify(this, r, s); if (s != null) { if (subj != null && !subj.unify(t.subj, r, s)) return false; if (obj != null && !obj.unify(t.obj, r, s)) return false; if (subj == null && near != null && !near.unify(t.near, r, s)) return false; if (t != deref()) deref().ref = t; bound = true; s.push(this, 0); } return true; } final void rewrite(boolean eu, Euler el, Parser np) { if (el.varid != -1) { Euler ex = el.subj.copy(); el.subj = np.parse("^^"); el.subj.subj = ex; el.subj.obj = np.parse(el.cverb); el.verb = el.cverb = "vv"; el.varid = -1; el.bound = true; } if (np.u == null || np.u.startsWith("_:engine_")) return; if (el.subj != null && el.subj.cverb == null) el.subj.verb = el.subj.cverb = (eu?"_:":"?v") + el.subj.uid + "_" + doc + "_"; if (el.obj != null && el.obj.cverb == null) el.obj.verb = el.obj.cverb = (eu?"_:":"?v") + el.obj.uid + "_" + 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.uid + "_" + 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.uid + "_" + 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.equals("^") && el.subj.subj != null && el.subj.subj.getFirst() == null && !el.verb.equals(LOGimplies) && !el.verb.equals(LOGnotImplies)) { Euler gr = el.subj.copy(); rewrite(eu, gr, np); Euler gv = np.parse(false, (eu?"_:":"?v") + gr.uid + "_" + 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.equals("^") && el.obj.obj != null && !el.verb.equals(LOGimplies) && !el.verb.equals(LOGnotImplies)) { Euler gr = el.obj.copy(); rewrite(eu, gr, np); Euler gv = np.parse(false, (eu?"_:":"?v") + gr.uid + "_" + 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.equals("!") && el.subj.subj != null && el.subj.subj.getFirst() == null && !el.verb.equals(LOGimplies) && !el.verb.equals(LOGnotImplies)) { Euler gr = el.subj.copy(); rewrite(eu, gr, np); Euler gv = np.parse(false, (eu?"_:":"?v") + gr.uid + "_" + 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.equals("!") && el.obj.obj != null && !el.verb.equals(LOGimplies) && !el.verb.equals(LOGnotImplies)) { Euler gr = el.obj.copy(); rewrite(eu, gr, np); Euler gv = np.parse(false, (eu?"_:":"?v") + gr.uid + "_" + 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; el.src = src; el.line = line; return el; } final Euler cvv() { Euler el = copy(); el.subj = copy(); el.subj.verb = el.subj.cverb = "^^"; el.subj.obj.verb = verb; el.subj.obj.cverb = cverb; el.verb = el.cverb = "vv"; 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) { if (!cverb.startsWith("_:") && cverb.indexOf('#') != -1) cverb = "?" + cverb.substring(cverb.indexOf('#') + 1, cverb.length() - 1); else if (!cverb.startsWith("_:") && cverb.indexOf(':') != -1) cverb = "?" + cverb.substring(cverb.indexOf(':') + 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 reorderPremis(Euler er) { Euler el = er.subj; Euler elc = null, elcp = null, elv = null, elvp = null; while (el != null) { if (er.obj.subj != null && el.subj.verb.equals(er.obj.subj.verb) && el.verb.equals(er.obj.verb)) { 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.subj = elc; } void synon(Euler t) { if (t.subj.deref().verb.equals("^^") || t.obj.deref().verb.equals("^^")) return; boolean w = !t.subj.deref().verb.startsWith(W3); 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)) ext.syn.put(s, o); for (Enumeration e = ext.syn.keys(); e.hasMoreElements(); ) { String k = (String)e.nextElement(); if (ext.syn.get(k).equals(s)) { if (!k.equals(o)) ext.syn.put(k, o); else ext.syn.remove(k); } } } else if (t.subj != null && t.obj == null && t.subj.subj == null && t.subj.obj == null) ext.syn.put(s, t); else if (t.subj == null && t.obj != null && t.obj.subj == null && t.obj.obj == null) ext.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 = ext.syn.get(t.verb); if (o != null) { if (o instanceof String) t.verb = (String)o; else t.verb = o.toString(); } } if (t.obj != null) syno(t.obj); } final Euler deref() { if (ref != null) return ref.deref(); else return this; } /** * string represention of this Euler obj * * @return string */ public final String toString() { if (ref != null && obj == null) return ref.toString(); if (subj == null && verb == null && obj == null) return "[]"; 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("!")) return subj + "!" + obj; if (cv != null && cv.equals("vv") && subj != null && subj.verb.equals("^^") && subj.subj.bound) return subj.subj + " " + subj.obj + " " + obj + ". "; if (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; 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()); 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); break; } r.append(' '); el = en; } r.append(')'); return r.toString(); } if (!sv && subj != null && subj.deref().subj != null && verb != null && subj.deref().verb != "!") { el = subj.deref(); while (el != null && el.verb != null) { r.append(el); el = el.near; } } else if (!sv && subj != null || !sv && subj != null && subj.deref().subj == null) { el = subj.deref(); r.append(el); } 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(' '); if (deref().cverb != null) r.append(deref().cverb); else r.append(cverb); r.append(' '); int i = r.length(); if (!ov && obj != null && obj.deref().subj != null && verb != null && obj.deref().verb != "!") { el = obj.deref(); while (el != null && el.verb != null) { r.append(el); el = el.near; } } else if (!ov && obj != null || !ov && obj != null && obj.deref().subj == null) { el = obj.deref(); r.append(el); } 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(el.deref().cverb).append(' '); r.append(el.obj); r.append(';'); el = el.near; } r.insert(0, '['); r.setCharAt(r.length() - 1, ']'); } return r.toString(); } 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 != null && (el.obj.verb.startsWith(MATH) || el.obj.verb.startsWith(STR))) { 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)); else if (Datatype.isNumeric(getType(s)) && Datatype.isNumeric(getType(o))) return new Double(getLit(s)).doubleValue() - new Double(getLit(o)).doubleValue(); else throw new NumberFormatException(); } final String fromWeb(String uri) { StringBuffer sb = new StringBuffer(); String rl = null; if (uri.startsWith("data:")) { ext.baseURI = "_:engine_" + ext.engine; return uri.substring(uri.indexOf(',') + 1); } else if (uri.startsWith("{")) { ext.baseURI = "_:engine_" + ext.engine; return uri.substring(1, uri.length() - 1); } else if (uri.startsWith("http:")) { try { ext.baseURI = uri.startsWith("http://localhost/euler.AskJena?fromWeb=")?"http://"+uri.substring(34):uri; if (!Configuration.getInstance().getRunLocal() || 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) { if (ext.baseURI.endsWith(".owl.n3") || ext.baseURI.endsWith(".rss.n3")) ext.baseURI = ext.baseURI.substring(0, ext.baseURI.length() - 3); if (ext.baseURI.endsWith(".n3")) ext.baseURI = ext.baseURI.substring(0, ext.baseURI.length() - 3) + ".rdf"; if (uri.endsWith(".owl.n3") || uri.endsWith(".rss.n3")) uri = uri.substring(0, uri.length() - 3); if (uri.endsWith(".n3")) uri = uri.substring(0, uri.length() - 3) + ".rdf"; return AskJena.fromWeb(!Configuration.getInstance().getRunLocal()?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('/')) + "/"; ext.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) { if (ext.baseURI.endsWith(".owl.n3") || ext.baseURI.endsWith(".rss.n3")) ext.baseURI = ext.baseURI.substring(0, ext.baseURI.length() - 3); if (ext.baseURI.endsWith(".n3")) ext.baseURI = ext.baseURI.substring(0, ext.baseURI.length() - 3) + ".rdf"; if (uri.endsWith(".owl.n3") || uri.endsWith(".rss.n3")) uri = uri.substring(0, uri.length() - 3); if (uri.endsWith(".n3")) uri = uri.substring(0, uri.length() - 3) + ".rdf"; return AskJena.fromWeb(uri); } } return sb.toString(); } final String toURI(Euler el) { if (el.verb == "^^" || el.verb == "^" || el.verb == "!") el = el.subj.deref(); if (el.obj != null) { StringBuffer sb = new StringBuffer("data:,"); for (Enumeration en = ext.ns.keys(); en.hasMoreElements(); ) { Object nsx = en.nextElement(); sb.append("@prefix ").append(nsx).append(' ').append(ext.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 ext.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.indexOf('#') != -1) s = s.substring(0, s.indexOf('#')); if (s.endsWith(".rdf")) s = s.substring(0, s.length() - 4) + ".n3"; else if (!s.endsWith(".n3") && !s.endsWith(".nt") && !s.startsWith("data:") && !s.startsWith("{")) 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(); } /** * Main method invoked via java Euler * * @param args [--think] [--nope] [--step count] [--debug] [--trace] axiom ... [--filter|--query] lemma */ public static void main(String[] args) { if (args.length == 0) { System.err.println("Version: " + Configuration.getInstance().getVersion() + "\nUsage: java [-Dhttp_proxy=%http_proxy%] Euler [--think] [--nope] [--step count] [--debug] [--trace] axiom ... [--filter|--query] lemma"); } else { try { 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--; } String c = e.toURI(np.parse('<' + args[n] + '>')); for (int j = 0; j < n; j++) { if (args[j].endsWith("-think")) Configuration.getInstance().setThink(true); else if (args[j].endsWith("-nope")) Configuration.getInstance().setProofExplanation(false); else if (args[j].endsWith("-step")) Configuration.getInstance().setSteps(Long.parseLong(args[++j])); else if (args[j].endsWith("-local")) Configuration.getInstance().setRunLocal(true); else if (args[j].endsWith("-debug")) StdOutputter.getInstance().setLogLevel(ILogger.FINE); else if (args[j].endsWith("-trace")) StdOutputter.getInstance().setLogLevel(ILogger.FINER); else if (!args[j].startsWith("-")) e.load(e.toURI(np.parse('<' + args[j] + '>'))); else if (args[j].endsWith("-graph")) { Euler el = new Euler(); el.load(e.toURI(np.parse('<' + args[++j] + '>'))); StringBuffer sb = new StringBuffer("data:,"); for (Enumeration en = el.ext.ns.keys(); en.hasMoreElements(); ) { Object nsx = en.nextElement(); sb.append("@prefix ").append(nsx).append(' ').append(el.ext.ns.get(nsx)).append(".\n"); } String s = el.ext.baseURI; while (el.near != null) { sb.append('{').append(el.near).append("} q:source <").append(s).append(">.\n"); el = el.near; } e.load(sb.toString()); } else if (args[j].endsWith("-filter") || args[j].endsWith("-query")) { Euler el = new Euler(); el.uid = -1; el.load(e.toURI(np.parse('<' + args[++j] + '>'))); StringBuffer sb = new StringBuffer("data:,"); for (Enumeration en = el.ext.ns.keys(); en.hasMoreElements(); ) { Object nsx = en.nextElement(); sb.append("@prefix ").append(nsx).append(' ').append(el.ext.ns.get(nsx)).append(".\n"); } while (el.near != null) { if (el.near.verb.equals(LOGimplies)) { for (Euler er = el.near.obj; er != null; er = er.near) { sb.append('{'); for (Euler ee = el.near.subj; ee != null; ee = ee.near) { e.rewrite(false, ee, np); sb.append(ee); } sb.append("} => {_:").append(el.near.uid).append(' ').append(Qselect).append(" {"); e.rewrite(false, er, np); sb.append(er).append("}}. "); } el = el.near; } else if (el.near.verb.equals(Qselect) && el.near.near.verb.equals(Qwhere)) { for (Euler er = el.near.obj; er != null; er = er.near) { sb.append('{'); for (Euler ee = el.near.near.obj; ee != null; ee = ee.near) { e.rewrite(false, ee, np); sb.append(ee); } sb.append("} => {").append(el.near.subj).append(' ').append(Qselect).append(" {"); e.rewrite(false, er, np); sb.append(er).append("}}. "); } el = el.near.near; } else el = el.near; } c = sb.toString(); e.load(c); } } e.prepare(); String p = e.proof(c); if (!Configuration.getInstance().getProofExplanation()) { Euler el = new Euler(); el.uid = -1; el.load("data:," + p); StringBuffer sb = new StringBuffer(); for (Enumeration enr = el.ext.ns.keys(); enr.hasMoreElements(); ) { Object nsx = enr.nextElement(); sb.append("@prefix ").append(nsx).append(' ').append(el.ext.ns.get(nsx)).append(".\n"); } sb.append('\n'); for (Euler eu = el; eu.near != null; eu = eu.near) { if (eu.near.verb.equals(Qselect)) { Euler en = eu.near.near; eu.near = eu.near.obj; eu.near.near = en; } } while (el.near != null) { Euler eu = el.near.near; while (eu != null) { if (eu.unify(el.near, e, null)) break; eu = eu.near; } if (eu == null && !el.near.cverb.equals("vv")) sb.append(el.near).append('\n'); el = el.near; } p = sb.toString(); } out.println(p); if (out != System.out) out.close(); } catch (Exception e) { e.printStackTrace(); } } } }