Re: [iris-reasoner-support] RuleValidator

[Murat K. <mur...@st...>]

Good Morning!

Now, this *is* tricky, but I read the new validator code and I think I 
understand it (and it ought to do what you've explained below). Thanks 
for clearing this up. As I hinted at in an earlier mail, I am producing 
a documentation for v0.5.7, focusing on architecture and the algorithms 
- so it is very possible, that I have further questions. :)

Also, if I find the time, I want to implement a IDataSource for a 
relational database, to be able to integrate RDBMS. In the head, there 
is no such thing yet. In this direction, there might be questions later, 
too.

Btw, is your answer to 1) "yes"? Just to be sure ...

Thanks,
Murat

Barry Bishop wrote:
> Hi Murat,
>
> Thanks once again for your most helpful code inspection!
>
> Yes, this is clearly a bug and I have investigated, created unit tests
> and fixed:
>
> See:
> https://sourceforge.net/tracker/index.php?func=detail&aid=2101601&group_id=167309&atid=842434
>
> It turns out to be surprisingly complicated to detect all variations of
> equality (unification) with function symbols. Here is the behaviour that
> is now supported:
>
> 1) All variables that appear in the rule head must be 'limited'
> 2) A variable is limited if it appears in a positive ordinary literal
> 3) A variable is limited if it is the result of an arithmetic built-in
> and all other terms are limited
> 4) A variable is limited if it is equated with another limited variable
>
> (Now it gets tricky)
>
> 5) Positive equality with constructed terms where the two arguments
> unify and the resulting variable mappings contain:
>   5a) variable maps to ground term -> variable is limited
>   5b) variable maps to another variable -> treated as equality of
> variables, i.e. if one of these variables is limited elsewhere then the
> other is also limited
>   5c) variable maps to constructed term (with variables) -> variable is
> limited if all variables present in the constructed term are limited
> elsewhere
>
> I hope this helps.
>
> If you find any more peculiarities then please keep let me know.
>
> Thanks once again,
> barry
>
>
>
> Murat Knecht wrote:
>   
>> Greetings, yet again,
>>
>> I would like to understand some more about the coding in the 
>> RuleValidator. If you could clear things up, I'd appreciate it.
>>
>> 1. If a literal contains constructed terms, you disable the built-in 
>> handling, effectively treating the literal as a non-builtin. I assume 
>> this is, because the arithmetic deduction (configurable by 
>> mAllowArithmeticPredicatesToImplyLimited) does not work with function 
>> symbols anyway. For example, it is hard to see where ADD(2, f(2,3), ?x) 
>> implies anything but an EvaluationException. So, these situations either 
>> trigger an UnsafeRuleException in the RuleValidator, or an 
>> EvaluationException later on, when the built-in is fed the function 
>> symbol. Is this train of thought correct?
>>
>> 2. If so, what about EQUAL, which does support function symbols 
>> (according to its documentation, anyways)? It does support computing the 
>> missing term, too, so I assume it is basically collateral damage as this 
>> scenario is not considered?
>>
>> Thanks,
>> Murat
>>
>>
>>
>> -------------------------------------------------------------------------
>> This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
>> Build the coolest Linux based applications with Moblin SDK & win great prizes
>> Grand prize is a trip for two to an Open Source event anywhere in the world
>> http://moblin-contest.org/redirect.php?banner_id=100&url=/
>> _______________________________________________
>> iris-reasoner-support mailing list
>> iri...@li...
>> https://lists.sourceforge.net/lists/listinfo/iris-reasoner-support
>>     
>
>