Hey Jos. Good to hear from you. See my comments inline. [hidden email] wrote: > Actually we use quite a lot of (even mutual) recursive rules and > you are right that existentials in the conclusion can complicate things. > Our experience is that a fresh bnode label per rule firing or using a > skolem function (like the euler builtin e:tuple) is giving too much > artificially introduced triples. On the other hand, a universal skolem > machine is doing a fine job, e.g. like explained in the last paper in > http://folli.loria.fr/cds/2006/courses/Bezem.Nivelle.IntroductionToAutomatedReasoning.pdf Yes, I have tried to glean the method from that last paper but unfortunately haven't been able to. Perhaps you can help decipher it or at least generalize the intuitions / motivations? > [[ > CL will never for any existential conclusion introduce a new witness if > there exists > already one. Skolem functions give new witnesses even if there exists > already one. > As a simple example, consider the coherent axiom p(x) → ∃y. p(y). This > is, of course, > an easy tautology. CL will never use it since the conclusion is > fulfilled whenever > the premiss is true. In clausifying it without thinking one starts by > partly spoiling > the dependence of the conclusion on the premiss: ∃y. (p(x) → p(y)). Then > one > makes the dependence of y on x explicit by introducing a Skolem function: > p(x) → p(f (x))). This is no longer a tautology, but a clause which > makes the > Herbrand universe infinite and can play a complicating role in the proof > search. > ]] > > A small test case that we ran using the euler.yap engine might > illustrate above: Yes, I get the general motivation for (as you explain above) the artificial nature of simply introducing a skolem term (or witness) in place of the existential variables in the head of rule since this doesn't account for already existing 'witnesses'. However, I'm having a hard time understanding Coherent Logic Theory well enough to determine how I might integrate it with my current inference strategy. > gives 2 triples > _:e0 :p :c. > _:e1 :p :c. > > gives only 1 triple > _:sk0 :p :c. (just thinking out loud) the difference seems to have some correspondence with the notion of lean graphs, correct? > I think that having the skolem machine effect in fuxi and cwm > is doable, well I'm convinced it is :) Excellent. Your confidence is encouraging. So perhaps you can help me out here :) >From what I can glean, coherent logic is an extension of resolution theory which is in the category of 'top-down' or theorem proving methods. Generally (as of late), I've been relying on the fact that (after magic set transformation of a set of definite horn clauses) evaluation via bottom-up methods (forward-chaining or fixed-point calculation) are equivalent to top-down methods (SLD resolution in particular) [Brass S. 1995]. So, I'm basically relying on a production rule algorithm (RETE-UL) to efficiently ( and via forward-chaining ) calculate a unique minimal model for the ruleset. I believe CWM does the same (i.e., rely on some form of RETE for efficiency). This is very much an operational approach and thus very different from the more declarative inference procedures such as tableux or resolution (Prolog) - despite the fact that their semantics coincide (in the case where the language corresponds to definite horn clause logic). With that in mind, I was hoping to extract from the CL paper, the specific aspects of the method that deal with the handling of the so called coherent disjunctions (where you have existentially quantified variables in the antecedent) but I wasn't able to. Could you point me to the specific sections in that paper? [Brass S. 1995] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.591 > > Kind regards, > > Jos De Roo | Agfa HealthCare > Senior Researcher | HE/Advanced Clinical Applications Research > T +32 3444 7618 > http://www.agfa.com/w3c/jdroo/ > > Quadrat NV, Kortrijksesteenweg 157, 9830 Sint-Martens-Latem, Belgium > http://www.agfa.com/healthcare > > > *Chimezie Ogbuji <[hidden email]>* > Sent by: [hidden email] > > 02/09/2009 03:40 AM > Please respond to > [hidden email] > > > > To > [hidden email] > cc > > Subject > Re: Optimizing for recursive rules > > > > > > > > > > > Hey Chris. See my response inline below > > Chris G. wrote: > > Suppose I have a rule that, when fired, creates a fact that might > > trigger the same rule. Such rules seem to slow FuXi down considerably > > (by about fact 250, or so), but when the recursive part is removed, it > > runs like lightning. Is there a way to optimize my rules and facts to > > avoid the cost incurred by recursive rules, or should we try and > > figure out a way to not need the recursive rules in the first place? > > Here is the rule that is causing the slowness: > > Unfortunately, recursive rules are inherently complex to compute for any > rule engine. Fuxi currently doesn't do anything special to handle > recursion. One thing that can be ruled out, however, is how much of the > slow down is primarily due to overhead (inefficiencies in the Python) > and this can be determined via profiling a run over recursive rules. > > Looking at the rule below, it looks like the problem is further > compounded by the fact that you have a BNode in the consequent / head of > the rule. FuXi will attempt to create a new name for the BNode every > time the rule is fired. This is only problematic if this then triggers > a cycle (where the same rule is fired, etc..). The only way this can be > dealt with is via a proper handling of BNodes in the consequent / head > of rules such as Jos pointed out in an earlier email. > > Overall, I'd suggest you look into trying to avoid recursive rules in > the first place. > > > > { > > ?sir a m:SequentialInferenceRelation. > > ?inf1 a m:Inference. > > ?inf1 has m:inference_name ?infName1. > > ?sir has m:inference_name_1 ?infName1. > > ?inf2 a m:Inference. > > ?inf2 has m:inference_name ?infName2. > > ?sir has m:inference_name_2 ?infName2. > > ?sir has m:new_inference_name ?newInfName. > > ?inf1 has m:inference_time ?infTime1. > > ?inf2 has m:inference_time ?infTime2. > > ?infTime2 math:greaterThan ?infTime1. > > } => { > > @forSome :inf. > > :inf a m:Inference. > > :inf has m:inference_name ?newInfName. > > }. > > -- Chimezie > > > > > > --~--~---------~--~----~------------~-------~--~----~ > You received this message because you are subscribed to the Google > Groups "fuxi-discussion" group. > To post to this group, send email to [hidden email] > To unsubscribe from this group, send email to > [hidden email] > For more options, visit this group at > http://groups.google.com/group/fuxi-discussion?hl=en > -~----------~----~----~----~------~----~------~--~--- > |
Hey Chimezie,
Let me first try to let some "running code" speak for itself :-) and point to the small section of Prolog code at % Skolem Euler Machine in http://eulersharp.sourceforge.net/2006/02swap/euler.yap sem/1 is like a forward chaining Horn engine producing the "trunk" deductive closure and sem/4 is the "branching" again forward chaining but taking care of false, possible and counter models. The trunk is like the main tape and the branches are like the split tapes of the skolem machine as is nicely depicted in http://www.csupomona.edu/~jrfisher/www/geolog/ Now to see whar really happens with the small test case of yesterday GIVEN :a :b :c. :d :e :c. {?X :b ?Y} => {_:Z :p ?Y}. {?X :e ?Y} => {_:Z :p ?Y}. QUERY {?X :p ?Y} => {?X :p ?Y}. I have just added some debug info and part of what it shows is enter branch [] . selecting rule pcl(<http://www.agfa.com/abc/try#b>(_12855,_12856),<http://www.agfa.com/abc/try#p>(_12858,_12856),<try.n3>) ... labelvars <http://www.agfa.com/abc/try#p>(sk(0),<http://www.agfa.com/abc/try#c>) ... assert step <http://www.agfa.com/abc/try#p>(sk(0),<http://www.agfa.com/abc/try#c>) enter branch [] . selecting rule pcl(<http://www.agfa.com/abc/try#b>(_12950,_12951),<http://www.agfa.com/abc/try#p>(_12953,_12951),<try.n3>) .. euler path so do not step in your own step <http://www.agfa.com/abc/try#p>(_12953,<http://www.agfa.com/abc/try#c>) . selecting rule pcl(<http://www.agfa.com/abc/try#e>(_12950,_12951),<http://www.agfa.com/abc/try#p>(_12953,_12951),<try.n3>) .. euler path so do not step in your own step <http://www.agfa.com/abc/try#p>(_12953,<http://www.agfa.com/abc/try#c>) So the key point is that an existential variable in the conclusion is kept as a prolog variable and labelvars is applied just in time before the triple is asserted. That is basically it and I think that it could fit with RETE quite well.. Kind regards, Jos De Roo | Agfa HealthCare Senior Researcher | HE/Advanced Clinical Applications Research T +32 3444 7618 http://www.agfa.com/w3c/jdroo/ Quadrat NV, Kortrijksesteenweg 157, 9830 Sint-Martens-Latem, Belgium http://www.agfa.com/healthcare
Hey Jos. Good to hear from you. See my comments inline. [hidden email] wrote: > Actually we use quite a lot of (even mutual) recursive rules and > you are right that existentials in the conclusion can complicate things. > Our experience is that a fresh bnode label per rule firing or using a > skolem function (like the euler builtin e:tuple) is giving too much > artificially introduced triples. On the other hand, a universal skolem > machine is doing a fine job, e.g. like explained in the last paper in > http://folli.loria.fr/cds/2006/courses/Bezem.Nivelle.IntroductionToAutomatedReasoning.pdf Yes, I have tried to glean the method from that last paper but unfortunately haven't been able to. Perhaps you can help decipher it or at least generalize the intuitions / motivations? > [[ > CL will never for any existential conclusion introduce a new witness if > there exists > already one. Skolem functions give new witnesses even if there exists > already one. > As a simple example, consider the coherent axiom p(x) → ∃y. p(y). This > is, of course, > an easy tautology. CL will never use it since the conclusion is > fulfilled whenever > the premiss is true. In clausifying it without thinking one starts by > partly spoiling > the dependence of the conclusion on the premiss: ∃y. (p(x) → p(y)). Then > one > makes the dependence of y on x explicit by introducing a Skolem function: > p(x) → p(f (x))). This is no longer a tautology, but a clause which > makes the > Herbrand universe infinite and can play a complicating role in the proof > search. > ]] > > A small test case that we ran using the euler.yap engine might > illustrate above: Yes, I get the general motivation for (as you explain above) the artificial nature of simply introducing a skolem term (or witness) in place of the existential variables in the head of rule since this doesn't account for already existing 'witnesses'. However, I'm having a hard time understanding Coherent Logic Theory well enough to determine how I might integrate it with my current inference strategy. > gives 2 triples > _:e0 :p :c. > _:e1 :p :c. > > gives only 1 triple > _:sk0 :p :c. (just thinking out loud) the difference seems to have some correspondence with the notion of lean graphs, correct? > I think that having the skolem machine effect in fuxi and cwm > is doable, well I'm convinced it is :) Excellent. Your confidence is encouraging. So perhaps you can help me out here :) >From what I can glean, coherent logic is an extension of resolution theory which is in the category of 'top-down' or theorem proving methods. Generally (as of late), I've been relying on the fact that (after magic set transformation of a set of definite horn clauses) evaluation via bottom-up methods (forward-chaining or fixed-point calculation) are equivalent to top-down methods (SLD resolution in particular) [Brass S. 1995]. So, I'm basically relying on a production rule algorithm (RETE-UL) to efficiently ( and via forward-chaining ) calculate a unique minimal model for the ruleset. I believe CWM does the same (i.e., rely on some form of RETE for efficiency). This is very much an operational approach and thus very different from the more declarative inference procedures such as tableux or resolution (Prolog) - despite the fact that their semantics coincide (in the case where the language corresponds to definite horn clause logic). With that in mind, I was hoping to extract from the CL paper, the specific aspects of the method that deal with the handling of the so called coherent disjunctions (where you have existentially quantified variables in the antecedent) but I wasn't able to. Could you point me to the specific sections in that paper? [Brass S. 1995] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.591 > > Kind regards, > > Jos De Roo | Agfa HealthCare > Senior Researcher | HE/Advanced Clinical Applications Research > T +32 3444 7618 > http://www.agfa.com/w3c/jdroo/ > > Quadrat NV, Kortrijksesteenweg 157, 9830 Sint-Martens-Latem, Belgium > http://www.agfa.com/healthcare > > > *Chimezie Ogbuji <[hidden email]>* > Sent by: [hidden email] > > 02/09/2009 03:40 AM > Please respond to > [hidden email] > > > > To > [hidden email] > cc > > Subject > Re: Optimizing for recursive rules > > > > > > > > > > > Hey Chris. See my response inline below > > Chris G. wrote: > > Suppose I have a rule that, when fired, creates a fact that might > > trigger the same rule. Such rules seem to slow FuXi down considerably > > (by about fact 250, or so), but when the recursive part is removed, it > > runs like lightning. Is there a way to optimize my rules and facts to > > avoid the cost incurred by recursive rules, or should we try and > > figure out a way to not need the recursive rules in the first place? > > Here is the rule that is causing the slowness: > > Unfortunately, recursive rules are inherently complex to compute for any > rule engine. Fuxi currently doesn't do anything special to handle > recursion. One thing that can be ruled out, however, is how much of the > slow down is primarily due to overhead (inefficiencies in the Python) > and this can be determined via profiling a run over recursive rules. > > Looking at the rule below, it looks like the problem is further > compounded by the fact that you have a BNode in the consequent / head of > the rule. FuXi will attempt to create a new name for the BNode every > time the rule is fired. This is only problematic if this then triggers > a cycle (where the same rule is fired, etc..). The only way this can be > dealt with is via a proper handling of BNodes in the consequent / head > of rules such as Jos pointed out in an earlier email. > > Overall, I'd suggest you look into trying to avoid recursive rules in > the first place. > > > > { > > ?sir a m:SequentialInferenceRelation. > > ?inf1 a m:Inference. > > ?inf1 has m:inference_name ?infName1. > > ?sir has m:inference_name_1 ?infName1. > > ?inf2 a m:Inference. > > ?inf2 has m:inference_name ?infName2. > > ?sir has m:inference_name_2 ?infName2. > > ?sir has m:new_inference_name ?newInfName. > > ?inf1 has m:inference_time ?infTime1. > > ?inf2 has m:inference_time ?infTime2. > > ?infTime2 math:greaterThan ?infTime1. > > } => { > > @forSome :inf. > > :inf a m:Inference. > > :inf has m:inference_name ?newInfName. > > }. > > -- Chimezie > > > > > > --~--~---------~--~----~------------~-------~--~----~ > You received this message because you are subscribed to the Google > Groups "fuxi-discussion" group. > To post to this group, send email to [hidden email] > To unsubscribe from this group, send email to > [hidden email] > For more options, visit this group at > http://groups.google.com/group/fuxi-discussion?hl=en > -~----------~----~----~----~------~----~------~--~--- > |
Free forum by Nabble | Edit this page |