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

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.

- 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).

- 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?

- 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.

-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
> 

-- 
Dr. Christopher A. Welty                    IBM Watson Research Center
+1.914.784.7055                             19 Skyline Dr.
cawelty@gmail.com                           Hawthorne, NY 10532
http://www.research.ibm.com/people/w/welty

Received on Friday, 19 September 2008 15:21:18 UTC