sio-dev
[Top] [All Lists]

Re: [sio-dev] Sharing and Integrating Ontologies

To: "[sio-dev] discussion" <sio-dev@xxxxxxxxxxxxxxxx>
Cc: architecture-ecosystem@xxxxxxx
From: Pat Hayes <phayes@xxxxxxx>
Date: Sat, 17 Apr 2010 02:54:09 -0500
Message-id: <E845F1B4-516A-4AB9-A068-4E007816A38B@xxxxxxx>
Um.. sorry if Ive been away from email for a while. Allow me to  
interject a little.    (01)

I'm rather fond of CL and of IKL, but I don't know that it is quite  
accurate to claim that IKL encompasses deontic *logic*. What  is true,  
I would claim, and I know this is a claim that requires a lot of  
justification which hasn't been given yet in any published forum, is  
that IKL (which, by the way, is in a strong sense reducible to CL  
itself, surprisingly) can re-describe deontic *facts* in a coherent  
way. That claim amounts to the idea that deontic assertions do not  
require a deontic *logic*, but can be expressed (in a suitable sense)  
in a classical assertional logic. This is similar to the older and  
less controversial claim that modal facts can be asserted in a non- 
modal logic, essentially by mapping the Kripke modal semantics into a  
FO theory (of 'possible worlds' or 'situations'). I would also argue  
that there are great advantages to such an approach, similarly to the  
arguments made by John McCarthy concerning modalities and modal logic;  
but again, I realize that this case has not yet been made, so I cannot  
expect others to blandly agree with me :-)    (02)

John's history is a little scrambled. Corrections noted below, purely  
in the interests of scholarly accuracy, in case someone one day  
decides to write a history of this stuff.    (03)

On Apr 16, 2010, at 10:21 AM, John F. Sowa wrote:    (04)

> Chris and David,
>
> JFS>> To support modal logics and other kinds of things, there is
>>> only one additional operator needed: the that-operator of IKL.
>
> CP> Does this support deontic logic?
>
> Short answer:  Yes.
>
> Longer answer with a bit of history:
>
> The old KIF had a powerful backquote operator, which very few
> people used because they had no idea what it could do, but which
> some people found extremely powerful for doing wondrous things.    (05)

True, KIF did, but KIF never provided an actual semantics for it. In  
fact, KIF was never, AFAIK, given a precise model-theoretic semantics.  
Certainly, no such model theory was ever published, and various claims  
(such as completeness of KIF) were made which would have been  
immediately seen  to be false if any precise model theory had ever  
been provided. KIF, as originally stated, for example, is not FOL. For  
a start, it is not compact.    (06)

> I used the backquote of KIF to support the metalevel features
> of conceptual graphs, and I wanted a similar feature in CL.    (07)

> But Pat H. and Chris M. didn't want to include it in the CL
> semantics because they didn't have a clean way to handle it.    (08)

There was at one time a fairly elaborate, if vague, proposal for what  
eventually became Common Logic, which involved a "core" logic and  
several extensions, including a typed extension and a meta-level  
extension. (http://cl.tamu.edu/minutes/stanford-minutes.html) But none  
of these more elaborate schemes were ever given precise flesh, and no  
actual technical proposals or drafts were ever submitted to the group.  
That group, in fact, never produced an actual proposal for a logic.  
The final version of the standard was not created by the group which  
had been discussing this elaborate scheme, but by a smaller ad-hoc  
group (which I convened) which decided to focus on what had been  
called the 'core' and get that done in full semantic detail, keeping  
it as simple as possible. And that is what became the text of the ISO  
standard. AFAIK, nobody has ever given a precise model theory for  
backquote: if we had waited for one to be created, we would still be  
waiting.    (09)

> Some people, including Doug Lenat    (010)

Doug was not a member of the group that created CL. Perhaps John is  
thinking of other discussions he may have had with Doug.    (011)

> and me, kept lobbying for
> something that had similar functionality.  Lenat said that
> he could use the context mechanism of conceptual graphs to
> represent CycL, but that mechanism required backquote.
>
> The IKRIS project, which included a number of participants
> who were involved with a variety of knowledge representation
> issues, included a subcommittee to develop an IKRIS Knowledge
> Language (IKL).  See
>
>    http://www.ihmc.us/users/phayes/IKL/SPEC/SPEC.html
>
> The only feature added to CL was the that-operator:
>
>    (exists (p) (= p (that (blue sky)))
>
> This says that there exists a proposition p, which is equal
> to the proposition that the sky is blue.    (012)

To be achingly precise, a proposition exists which has the same truth  
conditions as the CL sentence '(blue sky)'.    (013)

One way to think of this operator is that it is the classical lambda  
operator, but (very tightly) restricted to a (very) special case: the  
body must be a sentence, and the binding list must be empty. That is,  
it is a lambda abstraction which binds no variables. Thus, any such  
expression denotes a relation with no arguments, a zero-ary relation.  
This amounts to a thing which yields a truth-value when called with no  
arguments. Such entities exist in the CL model theory, and play  
exactly the role of propositions. The basic IKL assumption is that  
such entities exist for every sentential form that occurs inside a  
(that ...) expression. However, IKL does not sanction any inference  
rule of abstraction, even for these very stripped-down lambdas. This:    (014)

(blue sky)   |--   (exists (p)(= p (that (blue sky))))    (015)

is NOT a valid IKL inference rule. The only propositions that are  
required to exist are those that are needed to be the denotations of  
actual that-terms occurring in the axioms. This is what keeps IKL  
essentially first order.    (016)

It is important to note that these terms are not in any sense  
quotations. They do not denote sentences or indeed anything  
syntactical in nature. The propositions that they denote are ordinary  
semantic entities which already exist in CL interpretations.    (017)

BTW, the IKL model theory ensures that all instances of the Tarski "T- 
sentence" for propositions, which in IKL have the form    (018)

(iff <sentence> ((that <sentence>)))    (019)

are true in all interpretations. Moreover, IKL is completely type- 
free, and allows any sentence to be reified into a proposition using  
(that ...). Still, the logic is consistent. Here for example is the  
Liar paradox in IKL:    (020)

(= p (that (not (p))))    (021)

It is unsatisfiable, of course, but not paradoxical. There is simply  
no such p.    (022)


>  This operator
> also allows quantifiers outside the that-proposition to
> bind variables inside the proposition:
>
>    (exists (q x y z) (= q (+ x y z)))
>
> This feature gives Lenat and me the ability to define the
> metalevel operators and other kinds of definitions we would
> like to have.    (023)

I am surprised that it allows META level operators. It is most  
definitely not a form of quotation, and (as I said) it is eliminable,  
so that IKL (=, roughly, CL plus 'that') is in a sense reducible to  
CL. The sense involved here is similar to the observation  that full  
FOL is reducible to FOL without existentials, and in fact the  
reduction process is very like a kind of elaborate form of the Skolem  
reduction of FOL using 'skolem functions'.    (024)

What is definitely true, however, is that IKL can easily and smoothly  
encode all so-called 'context' or 'hybrid' or modal logical sentences,  
preserving their meanings, as long as those meanings are given using a  
Kripke-style semantics for the original languages. This was its  
primary utility for the IKRIS project, in fact.    (025)

Deontic sentences require a mapping which objectifies situations and  
classifies them as permitted,. obligatory, forbidden, etc.., which is  
a bit more of a stretch than the familiar Kripke/situational-context  
mapping, but I think is workable (though I have not, I confess, had  
time or funding support to be able to work out the full details.)    (026)

BTW, I have yet to see any clear justification for the need for  
deontic logic in any of these practical areas. The Business Rules  
community have bought into deontic logic, but I am not convinced that  
they really have good justifications for doing so. The actual use of  
doentic logic in the SBVR standard is almost pathetically inadequate.    (027)

Pat Hayes    (028)

>  In my summary of conceptual graphs, I summarize
> how I use this operator in CGs and their translation to IKL:
>
>    http://www.jfsowa.com/cg/cg_hbook.pdf
>
> See Section 4, pp. 16 to 22.  The following note (which is
> adapted from an excerpt in my KR book) has more detail
> about propositions, and we used it during our discussions
> about the IKL semantics:
>
>    http://www.jfsowa.com/logic/proposit.htm
>
> The following two papers (which I wrote before the IKL project)
> describes how metalevel operators about propositions can be
> used for a very flexible semantics, including the ability to
> define modal logics (including deontic):
>
>    http://www.jfsowa.com/pubs/laws.htm
>    Laws, Facts, and Contexts:
>    Foundations for Multimodal Reasoning
>
>    http://www.jfsowa.com/pubs/worlds.pdf
>    Worlds, Models, and Descriptions
>
> In the laws.htm paper, I defined Nested Graph Models (NGMs),
> which were inspired by conceptual graphs.  But they can also
> be represented by IKL.
>
> CP>> My impression is the deontic aspect of models in commercial
>>> systems is often not handled formally, but rather by informal
>>> craft and convention.
>
> DW> Perhaps I'm being a bit hard nosed, but if you know that
>> the modeling language has a convoluted intended interpretation,
>> why would you not define the Common Logic internal logic to be
>> exactly that interpretation?
>>
>> If you are going to use logic, I would think you would want
>> to be exact.
>
> The advantages and the difficulties of any formal definition
> are that they force vague and ambiguous informal practices to
> be stated in a single, unambiguous way.  The people who write
> the formal definitions must do a lot of hard work to make it
> precise while keeping it as close as possible to the informal
> intuitions.
>
> CP> Where a modelling language has an unclear on convoluted intended
>> interpretation (not uncommon) merely translating it into CL as
>> best one can will not resolve this. Though you could argue it is
>> a good first step to sorting things out.
>
> Vague, loose, and unclear specifications are usually implemented
> in ways that the designers were never clear about.  Furthermore,
> different implementers will interpret it in different ways.
>
> That is what happened to JavaScript, and users rarely wrote
> complex programs in JavaScript because they had no idea how
> different browsers (even different versions by the same vendor)
> would interpret the language.
>
> Note that JavaScript made a major leap in acceptability *after*
> ECMA defined the precisely specified ECMAScript and the major
> vendors implemented it.  That definition supported the huge
> increase in AJAX applications after Google Maps adopted it.
>
> I admit that the definitional work may be nontrivial, but
> languages above the IKL level will look exactly the same as
> they did before they were formally defined.  The important
> advantage is that different implementations that enforce the
> formal definitions will be guaranteed to be interoperable.
>
> CP> In the academic sphere there is also... research on
>> using Searlean performatives - which are, I believe, not
>> in CL.
>
> Yes, but they are supported by IKL.  By the way, I'd call
> them the Peirce-Wittgenstein-Austin-Searle performatives.
> At our VivoMind company, we use them in the Flexible Modular
> Framework:
>
>    http://www.jfsowa.com/pubs/arch.htm
>    Architectures for Intelligent Systems
>
>    http://www.jfsowa.com/pubs/paradigm.pdf
>    Two Paradigms Are Better Than One,
>    And Multiple Paradigms Are Even Better
>
> In the FMF, the pragmatics field (which specifies a
> performative) is separate from the language field.  That
> allows languages without a metalevel ability to be used
> in messages that have an attached performative, which
> indicates the purpose of the statement.
>
> CP> If we assume for a moment that we have formalised this,
>> then my guess is this revised modelling language would not
>> be a sub-set of CL as CL cannot (I believe) handle deontic
>> logic.
>
> Yes.  But note the use of metalevels in the laws.htm and
> worlds.pdf papers.  In the FMF, by the way, the metalevel
> doesn't go beyond a single proposition.  That alone is
> a big step for many applications.  But the laws and worlds
> papers show that a hierarchy of multiple metalevels can
> give you an enormous amount of expressive power.
>
> The that-operator of IKL can support those hierarchies.
>
> John
>
>
> _________________________________________________________________
> Msg Archives: http://ontolog.cim3.net/forum/sio-dev/
> Join Community: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
> Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/sio-dev/
> Unsubscribe: mailto:sio-dev-leave@xxxxxxxxxxxxxxxx
> Community Shared Files: http://ontolog.cim3.net/file/work/SIO/
> Community Wiki: 
>http://ontolog.cim3.net/cgi-bin/wiki.pl?SharingIntegratingOntologies
>
>    (029)

------------------------------------------------------------
IHMC                                     (850)434 8903 or (650)494 3973
40 South Alcaniz St.           (850)202 4416   office
Pensacola                            (850)202 4440   fax
FL 32502                              (850)291 0667   mobile
phayesAT-SIGNihmc.us       http://www.ihmc.us/users/phayes    (030)






_________________________________________________________________ 
Msg Archives: http://ontolog.cim3.net/forum/sio-dev/   
Join Community: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J 
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/sio-dev/  
Unsubscribe: mailto:sio-dev-leave@xxxxxxxxxxxxxxxx 
Community Shared Files: http://ontolog.cim3.net/file/work/SIO/ 
Community Wiki: 
http://ontolog.cim3.net/cgi-bin/wiki.pl?SharingIntegratingOntologies     (031)
<Prev in Thread] Current Thread [Next in Thread>