From: Chris Welty <cawelty@gmail.com>

Date: Mon, 18 May 2009 23:01:40 -0400

Message-ID: <4A122114.5020609@gmail.com>

To: kifer@cs.sunysb.edu

CC: "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>

Date: Mon, 18 May 2009 23:01:40 -0400

Message-ID: <4A122114.5020609@gmail.com>

To: kifer@cs.sunysb.edu

CC: "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>

Michael Kifer wrote: > Thanks, Chris, > > Here are my responses to your comments. > > > On Mon, 18 May 2009 15:55:06 -0400 > Chris Welty <cawelty@gmail.com> wrote: > >> Abstract: >> >> In the abstract and overview, I think the standard-speak used is too >> constraining regarding the requirement of future dialects to implement FLD: > > I already responded to that one in a previous email. > http://lists.w3.org/Archives/Public/public-rif-wg/2009May/0136.html > >> 2.2 Alphabet >> >> "Definition (Alphabet). The alphabet of the presentation language of RIF-FLD >> consists of the following disjoint subsets of symbols: " >> >> Common Logic allows variable symbols and constant symbols to overlap. Do the >> subsets need to be disjoint? All these types of things can be distinguished >> by their syntactic context. > > This is just an unnecessary complication, which buys you nothing. > In many respects, RIF is more general than Common Logic, and forcing one to > decide what is a variable and what isn't by the context is a huge nuisance. > In fact, you CANNOT determine what is a variable by the context alone. > Many rule languages omit quantifiers. How do you distinguish then? As you point out below, the choice should be up to a dialect. Allowing variable and constant symbols to overlap in FLD simply means that a dialect can make that choice, not that every dialect must support it. As it is, Common Logic cannot be expressed as an FLD dialect, and thus it is not more general. > Besides, we have already agreed early on that variables are prefixed with a ?, > and this is how one identifies them. We agreed on that for our existing dialects. I never agreed to that for all logic languages. I personally don't see why it is needed, unless you allow no quantifiers, in which case you do. Again, seems like its a choice in language design, not something to require of all. >> "A countably infinite set of quantifiers...where n ≥ 1" >> >> It seems strange to include the variables as part of the set of quantifiers. >> WHy aren't the quantifiers just Exists, Forall, ... > > Not strange at all. Are you proposing to define a special language for defining > quantifiers? No, but the "set of quantifiers" including distinguishing Forall x,y from Forall y,z and calling them different elements of the "set of quantifiers" just seems strange. I'm not calling it wrong, just strange. Forall and Exists seem like different elements of the set. This isn't a problem, I just found it odd. > Quantifiers can be very general with all kinds of variables in various places. > For instance, how would you define bounded quantifiers? You would need to > invent a separate sublanguage, but this sublanguage might turn out to be too > restrictive. What do you do then? Reconvene the WG to extend FLD? > Sounds like a huge complication with no visible benefits. I don't get your point, how does adding the variables to the elements of the set of quantifiers help you with bounded quantifiers? Bounded quantifiers need another argument with each variable. I guess I don't see how this helps you differentiate between different languages with different forms of quantification. > Remember that the presentation syntax allows one to "unpack" the variables from > the syntax, so the definition is just a general formal device. > >> 2.4 Terms >> >> "Positional terms in RIF-FLD generalize the regular notion of a term used in >> first-order logic. For instance, the above definition allows variables >> everywhere, as in ?X(?Y ?Z(?V "12"^^xs:integer)), where ?X, ?Y, ?Z, and ?V >> are > variables. Even ?X("abc"^^xs:string ?W)(?Y ?Z(?V "33"^^xs:integer)) is >> a positional term (as in HiLog [CKW93]). " >> >> This idea goes back at least as far as Enderton, 1972, and has been used in >> implemented systems such as SNePS and Conceptual Graphs in the 80s. Since >> Enderton published in '72 what was already a "well known encoding" of >> predicate variables in FOL, I don't think it's accurate to say this >> "generalizes...FOL". >> The fact is that this IS perfectly first-order. > > The idea goes back to Henkin. However, take another look at these terms and you > will see that some are not expressible in Henkin's syntax or in Common Logic. > It is in this context that HiLog is referred to. Second-order variables by > themselves are not worth bothering to reference, as this is common knowledge. > > You might be confusing first-order logic with first-order logic syntax. > The above paragraph says that these terms extend the terms used in first-order > logic. Nowhere it says that this extends first-order logic in general (because > this is a semantic, not syntactic matter). But FLD does, indeed, extend > first-order logic semantics, since it allows dialects to define inference using > intended models rather than all models. Yes of course, but this example is of positional terms and is completely first order. What about it do you consider non-Henkin (other than the datatypes), or non-CL? Again, I'm just talking about the positional terms item, not FLD terms in general. >> Thus it seems reasonable to just say something like: "Positional terms in >> RIF-FLD are quite general, and allow variables everywhere, as in ?X(?Y ?Z(?V >> "12"^^xs:integer)), where ?X, ?Y, ?Z, and ?V are variables. Even >> ?X("abc"^^xs:string ?W)(?Y ?Z(?V "33"^^xs:integer)) is a positional term (as >> in HiLog [CKW93], SNePS [SR87], and Common Logic [CL07]). " > > > See above. Also, SNePS has little to do with HiLog. I never said it did, just that this kind of syntactic freedom (to use variables in pretty much any position) was implemented in SNePS by 1985 at the latest, and probably earlier. >> 3.2 Truth Values > >> "RIF dialects can have additional truth values. For instance, the semantics >> of some versions of NAF, such as well-founded negation, requires three truth >> values: t, f, and u (undefined), where f <t u <t t. Handling of >> contradictions and uncertainty usually requires at least four truth values: >> t, u, f, and i (inconsistent). In this case, the truth order is partial: f <t >> u <t t and f <t i <t t. " > >> Since the document says the inverse operator needs to be defined, I suggest >> you define it here for these two examples. > > done > > >> 3.6 Interpretation of Non-document Formulas >> >> In a <t,u,f> valued dialect, I'm unsure what happens in this case: >> >> Exists(?x) P(?x) >> Exists(?x) P(a) :- P(?x) >> >> If this entails anything other than P(a), then we would have a hidden >> extension. > > Did you mean this? > > (*) P(a) :- Exists(?x) P(?x) No, I meant the example I gave, though (*) is equivalent in a first-order system to my second sentence, and the entailment of the two sentences would of course be P(a). I'd be happy with that rewrite, but now I don't know why the rewrite would make a difference. > First, let me say that FLD does not define entailment --- dialects do. > This is a MAJOR point. I'm just wondering what the sensible entailment in a well-founded semantics would be for that, and if it is the same as in a first order system. It seemed to me that you have a problem with a closed/open world and the entailments might be different. > Second, if you indeed meant Exists(?x) P(a) :- P(?x) then the above does not > entail anything useful (not even P(a)) in any reasonably defined dialect. > If you meant (*), then P(a) is entailed. For certain what I wrote entails P(a) in FOL, which is a pretty reasonably defined dialect. > Third, what did you mean by "anything other than P(a)"? > Of course, if it entails P(a) then it entails P(a) /\ P(a), P(a) \/ Exists(?x) > p(?x), etc. I fail to see your point here. I was wondering if it creates an "invisible extension" where e.g. the same rule means different things in different dialects. >> In general as reading I tried to think of myself using FLD to define a full >> first order (+ datatypes) dialect, but I was not able to get a clear idea of >> it, so I'm left unsure whether it would work. > > I am completely surprised. Which particular feature of FOL you had difficulty > with? > > This should be absolutely trivial. Just use signatures to restrict the syntax > (like we did in BLD) and then define entailment so that all semantic structures > would be considered intended. My point was not that I had trouble, my point was that I didn't actually do it. I feel like I would have had a more fundamental understanding of FLD if I had done that, but I didn't have time. I guess in some sense I feel like few if any will really understand FLD until they try to use it for something. >> I note that, like BLD, FLD avoids any notion of error. I understand why we >> did that for BLD, but wonder if more expressive and complicated dialects will >> want it, and whether FLD should support it. > > Do you have a proposal for how to do that specifically? > Of course one can think of many ways, but it is not particularly clear which is > the "right" one. > Given that our builtins do not support this notion, it is not even > clear what the utility of this thing would be. > > Furthermore, FLD is general enough to allow dialects to support certain types > of errors. For instance, they can introduce a new truth value (and a new > constant for functions that return errors). However, the wisdom of imposing > this through FLD is unclear to me. Well, sometimes you seem to miss the point of FLD (;-) - it shouldn't impose anything but rather provide a range of options to logic dialect designers. Anyway, I have no proposal for errors, just pointing out that some dialect designers might wish for it. I seem to recall the (lack of a) notion of error we are using in BLD was my proposal anyway, so I should be happy with it... -Chris -- 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/weltyReceived on Tuesday, 19 May 2009 03:02:22 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:47:56 UTC
*