Re: [Fwd: Re: [BLD] problem with definition of entailment]

On Fri, 19 Sep 2008 11:20:35 -0400
Chris Welty <cawelty@gmail.com> wrote:

> 
> I started digging into this today.
> 
> http://www.w3.org/2005/rules/wiki/BLD#Logical_Entailment
> 
> - The new definition of Models misses the definition of a model of a condition 
> formula, which is used in the new definition of logical entailment.  In the case 
> where we keep this document-entails-condition version of entailment, the 
> definition of model should be augmented.


This notion is not needed and so it is not there.


> - The new version still invokes the word query in a very informal way.  Perhaps 
> the reader should be forewarned that query is used informally and intuitively 
> here (yes its now better than it was before in this regard).

The word queries does not appear in any of the definitions. It appears in
discussions where this is used in its informal English meaning -- just like any
other English word that appears in those discussions.
Moreover, the use of this word is explained right there in the next sentence.


> - I like the simplicity of the new definitions, but I don't like nor understand 
> why you restricted the definition of entailment only to condition formulae.  I 
> think I'm OK with documents entailing formulae, but why not all (non-document) 
> formulae?  Currently, eg rule entailment is undefined.  Why do you think this is 
> better, Jos?


There is no need to define any other notion of entailment.
Compliance is required only for entailment of conditions, so only this is
really required. Other definitions are just red herring and distraction.
People might be scared or confused into thinking that they must implement that.
On top of this, this would require 2-3 all paragraphs of definitions, which are
completely superfluous.


> - I'm in agreement with Jos, that local constants cannot be accessed outside 
> their "scope" - at least that was the intuition of local constants I understood. 
>   However, in thinking about that issue it struck me that this might be a major 
> incompatibility with FOL.

You did not understand the issue.
Local constants CANNOT be accessed outside of their scope.

The only change is that in the old definition a query to a document, D, is
assumed to be outside of ANY scope, while in the new definition it is in the
scope of D. So, a query to D can see the local constants of D. But it cannot
see the local constants of the documents imported by D.

The old definition (where the query is outside of every scope) was flawed.  My
attempts to "fix" the definition with minimal changes were awkward and
unsatisfactory.  Jos proposed couple of amendments, which also were
flawed. There is a way to define this correctly, but it is more complex,
unnecessary, and, in my opinion, leads to counter-intuitive inferences.

For instance, if D = {p(_a)}, where _a is local, then the query
?- p(_a) fails (as is any other ground query).
But ?- p(?X) returns "yes" without binding ?X to anything.

This can be especially frustrating if the user actually stares at D and sees
p(_a) in D clear as day. But the query p(_a) still says "no".

From a practical point of view, whether it is Definition 1 or 2 does not
matter. Properly constructed RIF documents are not supposed to expose local
constants to querying (not by obscuring them, but by structuring the rules
properly).


	--michael  


> -Chris
> 
> 
> 
> Jos de Bruijn wrote:
> > Concerning the issue I mentioned in [1]:
> > 
> > Michael proposed a new definition [2] to overcome the issue.
> > I observed that the change in the definition implies two substantive
> > changes in the language.
> > The first change (a below) is probably not a problem, because
> > conformance is only defined for entailment of condition formulas, not
> > general formulas.
> > 
> > The second change (b below) is a bigger one: according to the old
> > definition (in LC), local constants are not preserved in entailment,
> > whereas in the new definition [2] they are.
> > 
> > 1) So, in LC:
> > 
> > <http://bla>( "a"^^rif:local )
> >   does not entail
> > <http://bla>( "a"^^rif:local )
> > 
> > 
> > 2) In [2]:
> > 
> > <http://bla>( "a"^^rif:local )
> >   entails
> > <http://bla>( "a"^^rif:local )
> > 
> > Michael is arguing that (2) is more intuitive and allows for a more
> > elegant definition of entailment.
> > I argue that (1) is more intuitive, because local constants should be
> > local (and can thus not be queried); I do not see a slightly less
> > elegant definition as a big problem.
> > 
> > Michael, did I describe the issue accurately?
> > 
> > 
> > Best, Jos
> > 
> > [1] http://lists.w3.org/Archives/Public/public-rif-wg/2008Sep/0106.html
> > [2]
> > http://www.w3.org/2005/rules/wiki/index.php?title=BLD&oldid=4669#Logical_Entailment
> > 
> > -------- Original Message --------
> > Subject: Re: [BLD] problem with definition of entailment
> > Date: Tue, 02 Sep 2008 10:40:05 +0200
> > From: Jos de Bruijn <debruijn@inf.unibz.it>
> > To: kifer@cs.sunysb.edu
> > References: <48AD85CB.1050800@inf.unibz.it>
> > <20080826233359.00ee8866@kiferserv>	<48B4FA9E.800@inf.unibz.it>
> > <20080829222704.72a09a46@kiferserv>
> > 
> > The new definition seems technically sound, but it represents two
> > significant changes:
> > a- entailment is not only defined for condition formulas, whereas
> > previously it was defined for general formulas
> > b- entailment now preserves names of local constants, whereas this was
> > not the case in the last call version of BLD.  So, the entailment in the
> > test case [1] does not hold in the last call version of BLD, but does
> > hold in the wiki version.
> > 
> > 
> > Concerning a: I actually think it is better to define entailment only
> > for condition formulas  (so I am in favor of this change), but this is a
> > pretty substantive change in the document, so I don't know whether we
> > can do this, procedurally.
> > 
> > Concerning b: this also represents a substantive change (so poses the
> > same procedural problems), plus I think local names should not be
> > preserved in entailment, so I am not in favor of this change.
> > 
> > Best, Jos
> > 
> > [1] http://www.w3.org/2005/rules/wiki/Local_Constant
> > 
> > Michael Kifer wrote:
> >> Rather than tinkering with these definitions, I got rid of the mention that
> >> each formula is in some document and instead defined what I really meant
> >> directly. Pls see.
> >>
> >> The reason I started talking about each formula being in a separate document
> >> was that I thought this simplifies things. But I now see that it only
> >> complicates them.
> >>
> >> michael
> >>
> >> On Wed, 27 Aug 2008 08:56:30 +0200
> >> Jos de Bruijn <debruijn@inf.unibz.it> wrote:
> >>
> >>> Michael Kifer wrote:
> >>>> Hi Jos,
> >>>> thanks for spotting this. It came from FLD, where anything can be part of a
> >>>> document. I do not want to complicate things too much, so would like to give a
> >>>> simplest definition. I can see two ways out:
> >>>>
> >>>> 1. A condition formula does not have to be in a document by itself, so no
> >>>>    changes are needed.
> >>>> 2. Define a query document (which I would like to avoid)
> >>>> 3. To change things as follows. Instead of requiring that every formula is
> >>>>    physically part of a document we can say that it is either part or is
> >>>>    *associated* with a unique document (without calling it a query document).
> >>>>
> >>>> I think the 3d option is the best.
> >>> In that case it would have to be defined what is meant with a formula
> >>> being associated with a document.
> >>> Personally I would prefer option 1. In that case only slight changes in
> >>> the definition of satisfaction in multi-structures would be required.
> >>>
> >>>
> >>> Best, Jos
> >>>
> >>>> 	--michael  
> >>>>
> >>>>
> >>>> On Thu, 21 Aug 2008 17:12:11 +0200
> >>>> Jos de Bruijn <debruijn@inf.unibz.it> wrote:
> >>>>
> >>>>> Michael,
> >>>>>
> >>>>> I found a problem with the definition of entailment in BLD. We want
> >>>>> entailment to be defined for any formula, specifically, the entailed
> >>>>> formula can be an arbitrary condition formula.  However, you state that
> >>>>> if a formula is not a document, then it belongs to a special query
> >>>>> document. Now, the notion of "query document" is not defined.  This is
> >>>>> one problem.
> >>>>> If we assume that the query document is simply a document, then we have
> >>>>> the problem that in BLD documents cannot contain condition formulas;
> >>>>> they can only contain facts and rules.  So, in that case entailment is
> >>>>> not defined for all condition formulas.
> >>>>> I suspect this is an error, so I would suggest to either defined
> >>>>> satisfaction for condition formulas or properly define the notion of
> >>>>> "query document".
> >>>>>
> >>>>>
> >>>>> Best, Jos
> > 
>

Received on Saturday, 20 September 2008 01:37:01 UTC