- From: Chris Welty <cawelty@gmail.com>
- Date: Fri, 19 Sep 2008 11:20:35 -0400
- To: Jos de Bruijn <debruijn@inf.unibz.it>, Michael Kifer <kifer@cs.sunysb.edu>
- CC: RIF <public-rif-wg@w3.org>
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