// $Id: Euler.cs 1295 2007-05-11 16:52:51Z josd $ // PxButton | build | csc /o /doc:Euler.xml *.cs | // PxButton | build2 | cscc -g *.cs -l /PNET/lib/cscc/lib/System.dll -l /PNET/lib/cscc/lib/System.Xml.dll && del Euler.exe && ren a.out.exe Euler.exe | using System; using System.Collections; using System.IO; using System.Net.Sockets; using System.Text; ///

Euler proof mechanism

/// Jos De Roo public class Euler { internal Euler subj = null; // RDF subject internal String verb = null; // RDF predicate as absoluteized verb internal Euler obj = null; // RDF object internal String cverb = null; // compact verb internal int varid = - 1; // variable id internal bool bound = false; // variable binding state internal bool vv = false; // variable verb state //#1.39 internal Euler refr = null; // to be dereferenced internal Euler premis = null; // to attach the premis internal Euler near = null; // to construct a conjunction internal Euler far; // to remember last clause internal Hashtable hshtNs = null; // to table namespaces internal Hashtable nsp = null; // to table namespace prefixes internal Hashtable hshtSyn = null; // to table synonyms internal Hashtable dds = null; // to table log:definitiveDocument and Service properties internal int varmax = 0; // maximum variable count internal String baseURI = null; // URI of base process internal Hashtable loaded = null; // to table document/engine pairs // removed internal long eng = engine; // engine number //#1.39 internal long engine = 1; // number of engines //#1.39 internal const String version = "R3484"; // REMOVED internal const long serialVersionUID = 1; //version number #1.39 internal const String IW = "constructs a proof engine Report r; public Euler() { r = new Report(); hshtNs = new Hashtable(); hshtSyn = new Hashtable(); // RegisterNamespaces(); far = this; } ///

loads all facts and rules acquired from the RDF URI in that proof engine

/// of the RDF resource public virtual void Load(String uri) { lock(this) { root = this; if (loaded == null) loaded = new Hashtable(); if (loaded['<' + uri + '>'] != null) return; String rk = fromWeb(uri); String u = baseURI; if (!uri.StartsWith("data:")) loaded['<' + baseURI + '>'] = this; ArrayList vt = new ArrayList(); Parser np = new Parser(rk, vt, this, u); // Refactor : Move this into the constructor of the EulerProver // we dont always need to have this data, not all Euler objects need new copies if (hshtNs == null) { hshtNs = new Hashtable(); nsp = new Hashtable(); hshtSyn = new Hashtable(); dds = new Hashtable(); // Refactor : RegisterNamespaces hshtNs["rdfs:"] = RDFS + "#>"; // #1.39 moved to RegisterNamespaces() hshtNs["log:"] = LOG + "#>"; hshtNs["iw:"] = IW + "#>"; // end Refactor : RegisterNamespaces } // Refactor : Move this into the constructor of the EulerProver StringBuilder gen = new StringBuilder("data:,"); if (debug || trace) Console.Error.WriteLine("load " + uri); while (true) { // Refactor : read eval and rewrite far.near = np.Parse(); if (far.near == null) break; while (far.near != null) { // Refactor : while loop over parsed data // Refactor : new Method LoadEvalForAll // Refactor : logForALL checking 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.Add(far.near.obj.verb); far.near = far.near.near; continue; } else { Euler fn = far.near; ArrayList wt = new ArrayList(); for (IEnumerator e = vt.GetEnumerator(); e.MoveNext(); wt.Add(e.Current)); while (fn != null && fn.verb.Equals(LOGforAll)) { if (!wt.Contains(fn.obj.verb)) wt.Add(fn.obj.verb); fn = fn.near; } if (wt.Count > varmax) varmax = wt.Count; far.near.subj.near = fn; far.near = far.near.subj; far.near.forX(false, wt); } } // Refactor : end of logForALL checking // Refactor : end Method LoadEvalForAll // New Function Rewrite after handling some predicates rewrite(true, far.near, np); // #1.39 new // Refactor : new Method LoadEvalPredicates // Refactor : new Method LoadEvalImplies // Refactor: Eval(LOGimplies), if (far.near.verb.Equals(LOGimplies)) { rewrite(false, far.near.subj, np); // #1.39 added new parameter to rewrite, TODO far.near.obj.premis = far.near.subj; if (far.near.obj.varid != -1) { // #1.39 added, TODO if (far.near.subj.verb.Equals(RDFSfyi)) far.near.subj.near.vv = true; // #1.39 added, TODO else if (far.near.subj.verb.Equals("")) far.near.subj.near.vv = true;// #1.39 added, TODO else far.near.subj.vv = true;// #1.39 added, TODO }// #1.39 added, TODO 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; } } // End of Implies // Refactor: end of Eval(LOGimplies), // Refactor : end Method LoadEvalImplies // Refactor : new Method LoadEvalOwlStuff // Refactor: Eval(RDFtype,RDFTPositiveEntailmentTest,OWLTPositiveEntailmentTest,OWLTInconsistencyTest,OWLTImportEntailmentTest,OWLTOWLforOWLTest) else if (far.near.verb.Equals(RDFtype) && (far.near.obj.verb.Equals(RDFTPositiveEntailmentTest) || far.near.obj.verb.Equals(OWLTPositiveEntailmentTest) || far.near.obj.verb.Equals(OWLTInconsistencyTest) || far.near.obj.verb.Equals(OWLTImportEntailmentTest) || far.near.obj.verb.Equals(OWLTOWLforOWLTest))) { // // #1.39 added, TODO Euler er = (Euler) loaded[far.near.subj.verb]; if (er == null) { er = new Euler(); loaded[far.near.subj.verb] = er; } er.cverb = far.near.obj.verb; engine++; } // Refactor: end of Eval(RDFtype,RDFTPositiveEntailmentTest,OWLTPositiveEntailmentTest,OWLTInconsistencyTest,OWLTImportEntailmentTest,OWLTOWLforOWLTest) // Refactor: Eval(RDFTinputDocument) else if (far.near.verb.Equals(RDFTinputDocument)) { if (loaded[far.near.subj.verb] == null) loaded[far.near.subj.verb] = new Euler(); //REMOVED #1.39 ((Euler)loaded[far.near.subj.verb]).cverb = "None"; } // Refactor: end of Eval(RDFTinputDocument) // Refactor: Eval(RDFTpremiseDocument) else if (far.near.verb.Equals(RDFTpremiseDocument)) { if (loaded[far.near.subj.verb] == null) loaded[far.near.subj.verb] = new Euler(); ((Euler)loaded[far.near.subj.verb]).Load(toURI(far.near.obj)); } // Refactor: end of Eval(RDFTpremiseDocument) // Refactor: Eval(OWLTimportedPremiseDocument) else if (far.near.verb.Equals(OWLTimportedPremiseDocument)) { if (loaded[far.near.subj.verb] == null) loaded[far.near.subj.verb] = new Euler(); ((Euler)loaded[far.near.subj.verb]).Load(toURI(far.near.obj)); } // Refactor: end of Eval(OWLTimportedPremiseDocument) // Refactor: Eval(RDFTentailmentRules),Eval(RDFD) else if (far.near.verb.Equals(RDFTentailmentRules) && far.near.obj.verb.StartsWith(RDFD)) { if (loaded[far.near.subj.verb] == null) loaded[far.near.subj.verb] = new Euler(); ((Euler)loaded[far.near.subj.verb]).Load("http://www.agfa.com/w3c/euler/xsd-rules.n3"); } // Refactor: end of Eval(RDFTentailmentRules),Eval(RDFD) /// BEGIN BLOCK NEW #1.39 added // Refactor: Eval(RDFTstatus),Eval(OBSOLETED) else if (far.near.verb.Equals(RDFTstatus) && far.near.obj.verb.Equals("\"OBSOLETED\"")) { if (loaded[far.near.subj.verb] == null) loaded[far.near.subj.verb] = new Euler(); ((Euler)loaded[far.near.subj.verb]).engine = 0; } // Refactor: end of Eval(RDFTstatus),Eval(OBSOLETED) // Refactor: Eval(OWLTlevel),Eval(OWLTLite) else if (far.near.verb.Equals(OWLTlevel) && far.near.obj.verb.Equals(OWLTLite) && nool) { if (loaded[far.near.subj.verb] == null) loaded[far.near.subj.verb] = new Euler(); ((Euler)loaded[far.near.subj.verb]).engine = 0; } // Refactor: end of Eval(OWLTlevel),Eval(OWLTLite) // Refactor: Eval(OWLTlevel),Eval(OWLTDL) else if (far.near.verb.Equals(OWLTlevel) && far.near.obj.verb.Equals(OWLTDL) && nood) { if (loaded[far.near.subj.verb] == null) loaded[far.near.subj.verb] = new Euler(); ((Euler)loaded[far.near.subj.verb]).engine = 0; } // Refactor: end of Eval(OWLTlevel),Eval(OWLTDL) // Refactor: Eval(OWLTlevel),Eval(OWLTFull) else if (far.near.verb.Equals(OWLTlevel) && far.near.obj.verb.Equals(OWLTFull) && noof) { if (loaded[far.near.subj.verb] == null) loaded[far.near.subj.verb] = new Euler(); ((Euler)loaded[far.near.subj.verb]).engine = 0; } // Refactor: end of Eval(OWLTlevel),Eval(OWLTFull) // Refactor: Eval(OWLequivalentClass) else if (far.near.verb.Equals(OWLequivalentClass)) gen.Append(far.near.subj + " " + RDFSsubClassOf + " " + far.near.obj + ". ") .Append(far.near.obj + " " + RDFSsubClassOf + " " + far.near.subj + ". "); // Refactor: end of Eval(OWLequivalentClass) // Refactor: Eval(OWLequivalentProperty) else if (far.near.verb.Equals(OWLequivalentProperty)) gen.Append(far.near.subj + " " + RDFSsubPropertyOf + " " + far.near.obj + ". ") .Append(far.near.obj + " " + RDFSsubPropertyOf + " " + far.near.subj + ". "); /// END OF #1.39 added // Refactor: end of Eval(OWLequivalentProperty) // Refactor: Eval(SubProperty) else if (far.near.verb.StartsWith(RDF + "#_")) gen.Append(far.near.verb + " " + RDFSsubPropertyOf + " " + RDFSmember + ". "); // end Refactor Eval(SubProperty) // Refactor : end Method LoadEvalOwlStuff // Refactor : end Method LoadEvalPredicates // BEGIN OF NEW BLOCK // report if (debug || trace) Console.Error.WriteLine("@@ assert " + far.near); far = far.near; // Refactor : Iterator over far } // while far.near != null Refactor : End of while loop over parsed data } // end of while(true) syno(this); String gener = gen.ToString(); if (!gener.Equals("data:,")) this.Load(gener); // line 261 // Recurse if (vt.Count > varmax) varmax = vt.Count; doc++; } // end of lock } ///

prepares that proof engine

public virtual void Prepare() { Console.Error.WriteLine("prepare!"); lock(this) { bool ot = think; long os = step; think = true; { // r.Prepare(engine,baseURI); } ///REMOVED #1.39: this.Load("data:,?x = ?x. "); // Refactor : new Method ProveSameAs() //Add new method to load constants into the proof Proof("data:,?s " + OWLsameAs + " ?o. "); // Refactor : end Method ProveSameAs() step = os; think = ot; Console.Error.WriteLine("syno"); syno(this); Console.Error.WriteLine("~syno"); } } ///

proofs a conjunction with that proof engine

/// of the RDF resource /// proof public virtual String Proof(String uri) { lock(this) { root = this; // NEW #1.39 TODO r.Proof(engine,uri); if (loaded == null) loaded = new Hashtable(); // NEW #1.39 TODO String cj = fromWeb(uri); String u = baseURI; // Refactor : Part of the Constructor of the Proof Object ArrayList vt = new ArrayList(); Parser np = new Parser(cj, vt, this, u); if (hshtNs == null) { hshtNs = new Hashtable(); this.nsp = new Hashtable(); hshtSyn = new Hashtable(); dds = new Hashtable(); hshtNs["rdfs:"] = RDFS + "#>"; hshtNs["log:"] = LOG + "#>"; hshtNs["iw:"] = IW + "#>"; } StringBuilder gen = new StringBuilder("data:,"); // Proof::Proof line 99 Euler goal = new Euler(); Euler g = goal; // Refactor : end of the Constructor of the Proof if (debug || trace) Console.Error.WriteLine("proof " + uri); // Refactor Proof::MainProofLoop while (true) { // line 918 Proof::MainProofLoop g.near = np.Parse(); if (g.near == null) break; // Refactor : iterator over Goal while (g.near != null && g.near.verb != null) { rewrite(true, g.near, np); // was rewrite(false, g.near, np); // call rewrite // refactor Begin ProofEval 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.Add(g.near.obj.verb); } else { Euler fn = g.near; ArrayList wt = new ArrayList(); for (IEnumerator e = vt.GetEnumerator(); e.MoveNext(); wt.Add(e.Current)); 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.Add(fn.obj.verb); fn = fn.near; } if (wt.Count > varmax) varmax = wt.Count; g.near = g.near.subj; Euler gn = g; while (gn.near != null) { gn.near.forX(false, wt); gn = gn.near; } gn.near = fn; } // end of else g = g.near; } // end if ForSome, forAll implies LogTruth else { // any other statemenst g.near.getX(false, vt); g.near.forX(false, vt); if (vt.Count > varmax) varmax = vt.Count; if (debug || trace) Console.Error.WriteLine("@@ query " + g.near); g = g.near; } if (g.subj.varid != -1 && (g.verb.Equals(RDFfirst) || g.verb.Equals(RDFrest) || g.verb.Equals(OWLoneOf) || g.verb.Equals(OWLintersectionOf) || g.verb.Equals(OWLunionOf))) gen.Append(g); // refactor End ProofEval } // end iterator } // end while true reorder(goal); syno(goal); String gener = gen.ToString(); if (!gener.Equals("data:,")) this.Load(gener); // line Euler::Proof 181 if (vt.Count > varmax) varmax = vt.Count; StringBuilder nsp = new StringBuilder(256); // Refactor : begin of EmitNamespaces IEnumerator en = (IEnumerator) hshtNs.Keys.GetEnumerator(); while (en.MoveNext()) { Object nsx = en.Current; nsp.Append("@prefix ").Append(nsx).Append(' ').Append(hshtNs[nsx]).Append(".\n"); } nsp.Append('\n'); // Refactor : end of EmitNamespaces // Refactor : Euler Proof Constructor int tab = 0; // line Euler:Proof.cs:192 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(); bool not = false; long istep = step; StringBuilder proof = new StringBuilder(4096); // Refactor : end Euler Proof Constructor // Refactor: EmitHeader begin line 209/1014 proof.Append("# Generated with http://www.agfa.com/w3c/euler/#").Append(version); proof.Append(" on ").Append(DateTime.UtcNow.ToString()).Append("\n"); // Refactor: end of EmitHeader int pn = 0; if (!nope) { // was loaded != null // Refactor :EmitSementicsOpen proof.Append("{\n (\n"); // Refactor :EmitKeys line 1007 IEnumerator enu = (IEnumerator) loaded.Keys.GetEnumerator(); while (enu.MoveNext()) proof.Append(' ').Append(enu.Current).Append('.').Append(LOGsemantics).Append("\n"); // Refactor :EmitSemanticsClose begin 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"); // Refactor :EmitSemanticsClose end } // Refactor :EmitKeys line 1007 // Refactor : Euler Proof Constructor proof.Append(nsp); int pns = proof.Length; proof.EnsureCapacity(proof.Length * 2); StringBuilder pp = new StringBuilder(4096); StringBuilder pc = new StringBuilder(4096); StringBuilder pm = new StringBuilder(4096); Hashtable pct = new Hashtable(); // Refactor : end of Euler Proof Constructor // Refactor : eval goal loop! Euler te = goal; while (te.near != null) { te.near = te.near.eval(vars, stack); te = te.near; // line 1183 } goal = goal.near; // line 1187 // Refactor : end of eval goal loop! // End of Proof::EvalGoals if (trace) Console.Error.WriteLine("[" + step + "]CALL: " + goal); long t = DateTime.Now.Ticks; // Refactor :Proof::CallGoal while (true) { // same as Proof::DoProof/CallGoal : line 258 // Refactor :Proof::IfGoalNotNull if (goal == null) { // same as Proof::IfGoalNotNull t = DateTime.Now.Ticks - t; // Refactor :Timer! if (proof.Length == pns) { // Refactor :Proof Emit Failed if (!nope) { //#new code 1.39 proof.Length = pn; proof.Append(WHYunknownBecause).Append("\n{\n"); }//#new code 1.39 proof.Append("# No proof found for "); // Refactor :end Proof Emit Failed } else { // Refactor : EmitKey IEnumerator sen = (IEnumerator) hshtSyn.Keys.GetEnumerator(); while (sen.MoveNext()) { Object sne = sen.Current; if (sne.Equals(hshtSyn[sne])) continue; proof.Append(sne); proof.Append(' '); proof.Append(OWLsameAs); proof.Append(' '); proof.Append(hshtSyn[sne]); proof.Append(" .\n"); } // Refactor : end of EmitKey proof.Append("# Proof found for "); } // Refactor : Emit Status report proof.Append(u); // #1.39 begin with StatusReport proof.Append(" in ").Append(step-istep).Append(step-istep==1?" step":" steps"); proof.Append(" (").Append((long)((step-istep)*10000000L/(t+100))).Append(" steps/sec)"); // @@ 100ns proof.Append(" using ").Append(engine).Append(engine==1?" engine":" engines"); if (!nope) proof.Append("\n}.\n"); // #1.39 end of StatusReport // Refactor : end of Emit Status report conc = pct; return proof.ToString(); } // if goal == null not = false; // BEGIN OF COMMENTED BLOCK // // Refactor : Emit Trace /// THIS WAS JUST PASTED IN!!!! try { if (goal.varid != - 1 && goal.subj != null && goal.obj != null) { Euler gn = goal.eval(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[pp.Length - 2] == '.' && pp[pp.Length - 1] == ' ') pp[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[pp.Length - 2] == '.' && pp[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.obj == 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) Console.Error.WriteLine("[" + step + "] " + goal); else if (goal.verb == STRconcatenation) { Euler el = goal.subj.deref(); StringBuilder sb = new StringBuilder("\""); while (el.getFirst() != null) { sb.Append(getLit(el.getFirst().deref())); el = el.getRest(); } sb.Append("\""); Euler er = np.Parse(String.Intern(sb.ToString())); 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.ToLower().Equals(ov.ToLower())) { 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.ToLower().Equals(ov.ToLower())) { 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 == MATHsum) { Euler el = goal.subj.deref(); double d = 0; while (el.getFirst() != null) { d += Double.Parse(getLit(el.getFirst().deref())); el = el.getRest(); } StringBuilder sb = new StringBuilder().Append(nat(goal.subj.deref(), d)); obj = np.Parse(String.Intern(sb.ToString())); 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 = Double.Parse(getLit(el.getFirst().deref())); el = el.getRest(); while (el.getFirst() != null) { d -= Double.Parse(getLit(el.getFirst().deref())); el = el.getRest(); } StringBuilder sb = new StringBuilder().Append(nat(goal.subj.deref(), d)); obj = np.Parse(String.Intern(sb.ToString())); 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 *= Double.Parse(getLit(el.getFirst().deref())); el = el.getRest(); } StringBuilder sb = new StringBuilder().Append(nat(goal.subj.deref(), d)); obj = np.Parse(String.Intern(sb.ToString())); 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 = Double.Parse(getLit(el.getFirst().deref())); el = el.near.obj; while (el.getFirst() != null) { d /= Double.Parse(getLit(el.getFirst().deref())); el = el.getRest(); } StringBuilder sb = new StringBuilder().Append(d); obj = np.Parse(String.Intern(sb.ToString())); 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 = Double.Parse(getLit(el.getFirst().deref())); el = el.near.obj; while (el.getFirst() != null) { d /= Double.Parse(getLit(el.getFirst().deref())); el = el.getRest(); } StringBuilder sb = new StringBuilder().Append(((int)d).ToString()); obj = np.Parse(String.Intern(sb.ToString())); 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 = Double.Parse(getLit(el.getFirst().deref())); el = el.getRest(); while (el.getFirst() != null) { d %= Double.Parse(getLit(el.getFirst().deref())); el = el.getRest(); } StringBuilder sb = new StringBuilder().Append(nat(goal.subj.deref(), d)); obj = np.Parse(String.Intern(sb.ToString())); 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 = Double.Parse(getLit(goal.subj.deref())); StringBuilder sb = new StringBuilder().Append(nat(goal.subj.deref(), -d)); obj = np.Parse(String.Intern(sb.ToString())); 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 = Double.Parse(getLit(goal.subj.deref())); StringBuilder sb = new StringBuilder().Append(nat(goal.subj.deref(), d<0?-d:d)); obj = np.Parse(String.Intern(sb.ToString())); 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 = Double.Parse(getLit(goal.subj.deref())); StringBuilder sb = new StringBuilder().Append(Math.Round(d)); obj = np.Parse(String.Intern(sb.ToString())); 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 = (double) Double.Parse(getLit(el.getFirst().deref())); el = el.getRest(); while (el.getFirst() != null) { d = Math.Pow(d, (double) Double.Parse(getLit(el.getFirst().deref()))); el = el.getRest(); } StringBuilder sb = new StringBuilder().Append(nat(goal.subj.deref(), d)); obj = np.Parse(String.Intern(sb.ToString())); 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(); } StringBuilder sb = new StringBuilder().Append(n); Euler er = np.Parse(String.Intern(sb.ToString())); 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) { bool ot = think; think = true; String p = this.Proof(toURI(goal.subj)); think = ot; StringBuilder sb = new StringBuilder().Append(conc.Count); Euler er = np.Parse(String.Intern(sb.ToString())); 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(String.Intern(gsv.Substring(0, gsv.IndexOf('#')) + '>')); 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++; bool 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(); 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(" "); pp.Append(p); if (tab == 0) pc.Append(p).Append('\n'); } if (goal.obj.ToString().IndexOf("Manifest") == -1) Console.Error.WriteLine((goal.obj.verb=="."?goal.obj.subj:goal.obj) + " <#PositiveEntailmentTest> " + (p.IndexOf("# Proof found")!=-1?"P":"NP")); think = ot; } else if ((goal.verb == RDFTconclusionDocument || goal.verb == RDFTinputDocument) && loaded[goal.subj.deref().verb] != null && ((Euler)loaded[goal.subj.deref().verb]).cverb != null && ((Euler)loaded[goal.subj.deref().verb]).engine != 0) { Euler er = (Euler)loaded[goal.subj.deref().verb]; if (er.cverb.Equals(OWLTInconsistencyTest)) er.Load(toURI(goal.obj)); if (er.cverb.StartsWith(RDFT)) er.Load(toURI(np.Parse(RDFS))); if (er.cverb.StartsWith(OWLT)) { er.Load(toURI(np.Parse(OWL))); er.Load(toURI(np.Parse(XSD))); er.Load(toURI(np.Parse(RDFS))); } er.Prepare(); String conc = toURI(goal.obj.deref()); if (conc.StartsWith("_:")) conc = "data:, _:X a " + RDFTFalseDocument + ". "; if (er.cverb.Equals(OWLTInconsistencyTest)) conc = "data:, _:X " + LOGinconsistentWith + " _:Y. "; String p = er.Proof(conc); pm.Append('\n'); for (int i = tab; i > 0; i--) pm.Append(" "); pm.Append(p); if (tab == 0) pc.Append(p).Append('\n'); Console.Error.WriteLine(goal.subj + " <" + er.cverb.Substring(er.cverb.IndexOf('#')) + " " + (p.IndexOf("# Proof found")!=-1?"P":"NP")); loaded.Remove(goal.subj.deref().verb); // @@ free memory } 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().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 == RDFSResource || 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.verb == RDFtype && goal.subj.deref().verb == "^^" && goal.subj.deref().obj.deref().verb == goal.obj.deref().verb || goal.verb.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(); bool b = mstep == -1 || step-istep < mstep*engine; bool d = dds[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.GetHashCode(); for (int i = 0; i < varmax; i++) vars[i] = null; if (ts.eval(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; 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) Console.Error.WriteLine("@@ cycle (2) " + ep); not = true; } else { ts = ts.premis; if (ts != null) { ts2 = new Euler(); ts1 = ts2; while (ts != null) { ts1.near = ts.eval(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[pp.Length - 2] == '.' && pp[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[pp.Length - 1] != '{') pp.Append(' '); pp.Append('{'); tab++; } else { if (goal.verb == OWLsameAs) synon(goal); if (pp.Length > 1 && pp[pp.Length - 2] == '.' && pp[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 (Exception exc) { Console.Error.WriteLine(exc.StackTrace); not = true; } /// end of huge block!!! if (trace) { if (!not && goal.verb != null) Console.Error.WriteLine("[" + step + "]EXIT: " + goal); else if (!not && goal.cverb != null) Console.Error.WriteLine(goal.cverb + "EXIT: " + goal.obj); else if (not && goal.verb != null) Console.Error.WriteLine("[" + step + "]FAIL: " + goal); else if (not && goal.cverb != null) Console.Error.WriteLine(goal.cverb + "FAIL: " + goal.obj); } if (goal.verb != null) { step++; if (debug && step % 1000000 == 0) Console.Error.WriteLine(step + " steps for " + u); } // Refactor : end of Emit Trace // Refactor : Iterate Goals goal = goal.near; // Refactor : end Iterate Goals if (trace && !not && goal != null && goal.verb != null) Console.Error.WriteLine("[" + 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) Console.Error.WriteLine("@@ continue"); pct[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.refr = null; } else { tab = b.varid; pc.Length = stack.pop().varid; pp.Length = stack.pop().varid; lr = stack.pop(); ts = stack.pop(); goal = stack.pop(); if (trace) Console.Error.WriteLine("[" + step + "]REDO: " + goal); break; } } } } } } internal Euler eval(Euler[] v, Stack s) { if (refr != null && obj == null) return refr.eval(v, s); if (bound && varid == - 1 && obj == null) return this; if (varid != -1 && v[varid] != null && v[varid].vv) { Euler t = new Euler(); if (subj != null) t.subj = subj.eval(v, s); if (obj != null) t.obj = obj.eval(v, s); t.verb = v[varid].deref().verb; t.cverb = v[varid].deref().cverb; t.varid = v[varid].deref().varid; t.bound = true; return t; } if (varid != - 1 && v[varid] == null) v[varid] = new Euler(); if (obj != null) { Euler t = new Euler(); if (subj != null) t.subj = subj.eval(v, s); if (obj != null) t.obj = obj.eval(v, s); t.verb = verb; t.cverb = cverb; t.varid = varid; if (v != null && !bound && varid != - 1) { if (v[varid] != t) t.refr = v[varid]; t.bound = true; s.push(t, 0); } else t.bound = true; t.vv = vv; if (subj == null && obj != null && near != null) t.near = near.eval(v, s); else t.near = near; return t; } v[varid].verb = verb; v[varid].cverb = cverb; v[varid].varid = varid; return v[varid]; } internal bool unify(Euler t, Euler r, Stack s) { if (t == null) return false; if (refr != null && obj == null) return refr.unify(t, r, s); if (t.refr != null && t.obj == null) return unify(t.refr, 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(obj.deref().verb) && Datatype.IsNumeric(t.obj.deref().verb))) return Datatype.Compare(obj.deref().verb, r.getLit(this), 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().refr = t; bound = true; s.push(this, 0); } return true; } internal bool oc(int vi) { if (refr != null) return refr.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); } internal void rewrite(bool eu, Euler el, Parser np) { 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.GetHashCode() + "_" + 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.GetHashCode() + "_" + 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.GetHashCode() + "_" + 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.GetHashCode() + "_" + 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.GetHashCode() + "_" + 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.GetHashCode() + "_" + 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; } } internal 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 (refr != el) el.refr = refr; el.premis = premis; if (near != null) el.near = near.copy(); el.far = far; return el; } internal void getX(bool f, ArrayList wt) { if (subj != null) subj.getX(true, wt); if (verb != null && (verb.StartsWith("_:") || verb.StartsWith("?")) && !wt.Contains(verb)) wt.Add(verb); if (obj != null) obj.getX(true, wt); if (f && near != null) near.getX(f, wt); } internal void forX(bool f, ArrayList wt) { if (subj != null) subj.forX(true, wt); if (verb != null && wt.Count > 0 && 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); } internal 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; } internal void synon(Euler t) { String s = t.subj.deref().verb; String o = t.obj.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)) hshtSyn[s] = o; for (IEnumerator e = (IEnumerator) ((Hashtable)hshtSyn.Clone()).Keys.GetEnumerator(); e.MoveNext(); ) { String k = (String) e.Current; if (hshtSyn[k] != null && hshtSyn[k].Equals(s)) { if (!k.Equals(o)) hshtSyn[k] = o; else hshtSyn.Remove(k); } } } else if (t.subj != null && t.obj == null && t.subj.subj == null && t.subj.obj == null) hshtSyn[s] = t; else if (t.subj == null && t.obj != null && t.obj.subj == null && t.obj.obj == null) hshtSyn[o] = t; } internal void syno(Euler t) { for (Euler el = t; el != null; el = el.near) synt(el); } internal void synt(Euler t) { if (t.subj != null) syno(t.subj); if (t.verb != null) { Object o = this.hshtSyn[t.verb]; if (o != null) { if (o is String) t.verb = (String) o; else t.verb = o.ToString(); } t.verb = String.Intern(t.verb); } if (t.obj != null) syno(t.obj); } internal Euler deref() { if (refr != null) return refr.deref(); else return this; } internal String stringf(bool f, int n) { if (refr != null && obj == null) return refr.stringf(f, n); String cv = debug?deref().verb: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 "[]"; if (cv.Equals(RDFnil)) return "()"; return cv; } Euler el = deref(); Euler en = null; StringBuilder r = new StringBuilder(64); bool sv = subj != null && subj.refr == null && subj.subj == null && subj.cverb != null && subj.cverb.Equals("[]") && subj.obj == null; bool ov = obj != null && obj.refr == null && obj.subj == null && obj.cverb != null && obj.cverb.Equals("[]") && obj.obj == null; bool b = verb != null && !verb.Equals(MATHproofCount) && !verb.Equals(LOGimplies) && !verb.Equals(LOGincludes) && !verb.Equals(LOGnotIncludes) && !verb.Equals(LOGinconsistentWith); 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, n++)); if (r.Length > 1 && (r[r.Length - 2] == '.' && r[r.Length - 1] == ' ' || r[r.Length - 1] == ';')) { if (r[i] != ' ') { r.Insert(i, '{'); r[r.Length - 2] = '}'; } else { r.Insert(i, '['); r[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, n++)); break; } r.Append(' '); el = en; } r.Append(')'); return r.ToString(); } if (!sv && subj != null && verb != null && verb.Equals(LOGimplies) && subj.verb != ".") { el = subj.deref(); while (el != null) { r.Append(el.stringf(b && el.subj != null && el.obj != null, n++)); 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, n++)); } if (r.Length > 1 && (r[r.Length - 2] == '.' && r[r.Length - 1] == ' ' || r[r.Length - 1] == ';')) { if (r[0] != ' ') { r.Insert(0, '{'); r[r.Length - 2] = '}'; } else { r.Insert(0, '['); r[r.Length - 1] = ']'; } } r.Append(' '); r.Append(debug?deref().verb:deref().cverb); if (n % 2 == 0) { r.Append('\n'); for (int i = n; i >= 0; i--) r.Append(" "); n++; } else r.Append(' '); int i2 = r.Length; if (!ov && obj != null && verb != null && verb.Equals(LOGimplies) || !ov && obj != null && obj.deref().subj == null) { el = obj.deref(); r.Append(el.stringf(b && el.subj != null && el.obj != null, n++)); } else if (!ov && obj != null) r.Append(obj.stringf(b && obj.subj != null && obj.obj != null, n++)); if (r.Length > 1 && (r[r.Length - 2] == '.' && r[r.Length - 1] == ' ' || r[r.Length - 1] == ';')) { if (r[i2] != ' ') { r.Insert(i2, '{'); r[r.Length - 2] = '}'; } else { r.Insert(i2, '['); r[r.Length - 1] = ']'; } } if (!sv && subj != null) 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, n++)); r.Append(';'); el = el.near; } r.Insert(0, '['); r[r.Length - 1] = ']'; } return r.ToString(); } ///

string represention of this Euler object

/// string public override String ToString() { return stringf(false, 0); } internal 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; } internal 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; } internal 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 - 6); if (s.IndexOf('"') != -1) return s.Substring(s.IndexOf('"') + 1, s.LastIndexOf('"') - s.IndexOf('"') - 1); return s; } internal double mathCompare(Euler el) { Euler s = el.subj.deref(); Euler o = el.obj.deref(); if (s.verb == "^^" && o.verb == "^^" && (s.obj.deref().verb == o.obj.deref().verb || Datatype.IsNumeric(s.obj.deref().verb) && Datatype.IsNumeric(o.obj.deref().verb))) return Datatype.Compare(s.obj.deref().verb, getLit(s), getLit(o)); return Double.Parse(getLit(s)) - Double.Parse(getLit(o)); } internal void whysub(StringBuilder 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[sb.Length - 2] == '.' && sb[sb.Length - 1] == ' ') sb.Insert(sb.Length - 2, '}'); else sb.Append("}. "); } else sb.Append(this); } internal void whysubst(StringBuilder sb, int tab) { if (subj.varid != -1) { sb.Append("[ ").Append(IWV).Append(" \"").Append(subj.cf()).Append("\"] = ").Append(subj.deref()).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) { sb.Append("[ ").Append(IWV).Append(" \"").Append(obj.cf()).Append("\"] = ").Append(obj.deref()).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()); } internal String cf() { if (subj == null && verb == RDFfirst) return this.ToString(); if (cverb == "^^") return subj + "^^" + obj; else return cverb; } internal String fromWeb(String uri) { StringBuilder sb = new StringBuilder(); String rl = null; if (uri.StartsWith("data:")) return uri.Substring(uri.IndexOf(',') + 1); else if (uri.StartsWith("http:")) { try { if (!uri.StartsWith("http://localhost/AskJena?fromWeb=")) baseURI = uri; if (!local || uri.StartsWith("http://localhost")) { Uri r = new Uri(uri); String p = r.PathAndQuery; String hp = Environment.GetEnvironmentVariable("http_proxy"); if (hp != null && !hp.Equals("") && !hp.Equals("%http_proxy%") && !uri.StartsWith("http://localhost")) { r = new Uri(hp); p = uri; } TcpClient so = new TcpClient(r.Host, r.Port == - 1?80:r.Port); //so.NoDelay.Enabled = true; StreamWriter pw = new StreamWriter((Stream) so.GetStream()); pw.WriteLine("GET " + p + " HTTP/1.0"); pw.WriteLine("Host: " + r.Host); pw.WriteLine(""); pw.Flush(); StreamReader br = new StreamReader((Stream) so.GetStream()); if ((rl = br.ReadLine()).IndexOf("200") == - 1) throw new SystemException(rl); while (!br.ReadLine().Equals("")); while ((rl = br.ReadLine()) != null) { sb.Append(rl); sb.Append('\n'); } so.Close(); } else { StreamReader br = new StreamReader(uri.Substring(6)); while ((rl = br.ReadLine()) != null) { sb.Append(rl); sb.Append('\n'); } br.Close(); } } catch (Exception) { if (uri.StartsWith("http://localhost")) throw new SystemException(uri); return fromWeb("http://localhost/AskJena?fromWeb=" + (!local?uri:uri.Substring(6))); } } else { if (uri.StartsWith("file:")) uri = uri.Substring(uri.IndexOf(':') + 1); if (uri.IndexOf('#') != - 1) uri = uri.Substring(0, uri.LastIndexOf('#')); try { String path = Directory.GetCurrentDirectory().Replace(Path.DirectorySeparatorChar, '/'); path = path.Substring(path.IndexOf('/')) + "/"; baseURI = "file:" + ((uri[0] == '/' || uri[1] ==':') ? "" : path) + uri; StreamReader br = new StreamReader(uri); while ((rl = br.ReadLine()) != null) { sb.Append(rl); sb.Append('\n'); } br.Close(); } catch (Exception) { return fromWeb("http://localhost/AskJena?fromWeb=" + uri); } } return sb.ToString(); } internal String toURI(Euler el) { if (el.verb == "^^" || el.verb == "^" || el.verb == ".") el = el.subj; if (el.obj != null) { StringBuilder sb = new StringBuilder("data:,"); for (IEnumerator en = (IEnumerator) hshtNs.Keys.GetEnumerator(); en.MoveNext(); ) { Object nsx = en.Current; sb.Append("@prefix ").Append(nsx).Append(' ').Append(hshtNs[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[0] == '<') s = s.Substring(1, s.Length - 2); if (s[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; } } internal String nat(Euler el, double d) { if (el.getFirst() == null && getLit(el.deref()).IndexOf('.') != -1) return d.ToString(); while (el.getFirst() != null) { if (getLit(el.getFirst().deref()).IndexOf('.') != -1) return d.ToString(); el = el.getRest(); } return ((int)d).ToString(); } internal bool isNumeral() { try { Double.Parse(verb); return true; } catch (Exception) { if (debug || trace) Console.Error.WriteLine("** " + verb + " not a numeral"); return false; } } internal String toHex(String s) { StringBuilder sb = new StringBuilder(); for (int i = 0; i < s.Length; i++) sb.Append(Convert.ToString(s[i], 16)); return sb.ToString(); } ///

Main method invoked via Euler

/// [--think] [--nope] [--step count] [--debug] [--trace] axiom ... lemma [STAThread] public static void Main(String[] args) { if (args.Length == 0) Console.Error.WriteLine("Euler [--think] [--nope] [--step count] [--debug] [--trace] axiom ... lemma"); else { try { step = 1; trace = false; think = false; TextWriter outp = Console.Out; Euler e = new Euler(); Parser np = new Parser(); int n = args.Length - 1; if (args[n].StartsWith(">")) { outp = new StreamWriter(new FileStream(new FileInfo(args[n].Substring(1)).FullName, FileMode.Create)); 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("-nool")) nool = true; else if (args[j].EndsWith("-nood")) nood = true; else if (args[j].EndsWith("-noof")) noof = true; else if (args[j].EndsWith("-step")) mstep = Int64.Parse(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] + '>')));// line 966 } e.Prepare(); outp.WriteLine(e.Proof(e.toURI(np.Parse('<' + args[n] + '>')))); if (outp != Console.Out) outp.Close(); } catch (Exception e) { Console.Error.WriteLine(e.StackTrace); } } } }