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

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

-- 
Jos de Bruijn            debruijn@inf.unibz.it
+390471016224         http://www.debruijn.net/
----------------------------------------------
No one who cannot rejoice in the discovery of
his own mistakes deserves to be called a
scholar.
  - Donald Foster

-- 
                         debruijn@inf.unibz.it

Jos de Bruijn,        http://www.debruijn.net/
----------------------------------------------
One man that has a mind and knows it can
always beat ten men who haven't and don't.
  -- George Bernard Shaw