ontolog-admin
[Top] [All Lists]

Re: [ontolog-admin] [ontolog-forum] Type Systems for Common Logic

To: "Dr. Mohammad Reza Beik Zadeh" <mohammad.reza@xxxxxxxx>
Cc: "[ontolog-admin] forum" <ontolog-admin@xxxxxxxxxxxxxxxx>
From: Peter Yim <peter.yim@xxxxxxxx>
Date: Sun, 21 Aug 2011 20:19:57 -0700
Message-id: <CAGdcwD0Ta0jf+BjFTuxoKtpp7j4f42dt0ZQjvKp3uhBGSNAT-g@xxxxxxxxxxxxxx>
Dear Dr. Mohammad Reza Beik Zadeh    (01)


Thank you very much for your post to the [ontolog-forum] mailing list.
As you are aware, Ontolog is an "open" virtual community of practice,
operating in an "open" collaborative work environment (CWE), which
serves as its dynamic knowledge repository. Upon this CWE, we are
collectively building a body of knowledge for the ontology domain.    (02)

We do have an open IPR policy (see:
http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid32) which
applies to all participation in Ontolog activities. It specifically
state that those who are unable to contribute under the open licensing
arrangements citing in our IPR Policy should refrain from contributing
to the [ontolog-forum] content.    (03)

As such, I am writing to let you know that the
disclaimer/confidentiality statement at the bottom of your message
(probably just automatically inserted by your institution) is
something that should *not* be included as part of the contribution.
Therefore, please suppress them before you make future posts. (If
possible, a short statement from you asking people to ignore that
statement from your last message is appreciated too.)  ... Some
members have found it easier to just subscribe with an alternate
e-mail address that is operated outside of their institutional
firewalls. You might consider that too.    (04)

Thank you for your attention.    (05)


Regards.  =ppy    (06)

Peter P. Yim    (07)

Co-convener,
Ontolog Forum
http://ontolog.cim3.net/wiki/
--    (08)


On Sun, Aug 21, 2011 at 7:34 PM, Dr. Mohammad Reza Beik Zadeh
<mohammad.reza@xxxxxxxx> wrote:
> Dear All
> I am looking for a good review paper, Book or presentation on challenges of 
>current semantic technology languages and features of an ideal semantic 
>technology language.
> May I have your guidance?
>
> Beik
>
> -----------------------------------------------
>  A strategic agency under MOSTI
>  www.mimos.my
> -----------------------------------------------
>
> ------------------------------------------------------------------
> -
> -
> DISCLAIMER:
>
> This e-mail (including any attachments) is for the addressee(s)
> only and may contain confidential information. If you are not the
> intended recipient, please note that any dealing, review,
> distribution, printing, copying or use of this e-mail is strictly
> prohibited. If you have received this email in error, please notify
> the sender  immediately and delete the original message.
> MIMOS Berhad is a research and development institution under
> the purview of the Malaysian Ministry of Science, Technology and
> Innovation. Opinions, conclusions and other information in this e-
> mail that do not relate to the official business of MIMOS Berhad
> and/or its subsidiaries shall be understood as neither given nor
> endorsed by MIMOS Berhad and/or its subsidiaries and neither
> MIMOS Berhad nor its subsidiaries accepts responsibility for the
> same. All liability arising from or in connection with computer
> viruses and/or corrupted e-mails is excluded to the fullest extent
> permitted by law.    (09)


> -----Original Message-----
> From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx 
>[mailto:ontolog-forum-bounces@xxxxxxxxxxxxxxxx] On Behalf Of John F. Sowa
> Sent: Sunday, 21 August, 2011 2:45 AM
> To: [ontolog-forum]
> Cc: rick@xxxxxxxxxxxxxx
> Subject: [ontolog-forum] Type Systems for Common Logic
>
> In the recent discussions, I was responding to comments about the
> "type free" Common Logic, but I didn't bring up a very important
> point:  Conceptual Graphs have had a very rich type system from
> Day 1 -- actually from the first published paper about CGs in 1976:
>
>     http://www.jfsowa.com/pubs/cg1976.pdf
>     Conceptual Graphs for a Database Interface
>
> In that paper, I called CGs a version of sorted logic.  But for the
> book version in 1984, I used the term 'type' rather than 'sort'.
> Following is a brief summary of the CG type system, which evolved
> from the original sorted logic in the 1976 paper:
>
>  1. A partial ordering of types by generalization and specialization.
>     Type T1 is a generalization of T2 (and T2 is a specialization of
>     T1) iff for every model, every instance of T2 is an instance of T1.
>
>  2. The universal type, which is true of everything in every model,
>     is a generalization of every type.  The absurd type, which is
>     true of nothing, is a specialization of every type.
>
>  3. Canonical graphs, which specify type constraints for well formed
>     CGs, are a generalization of the signatures used for specifying
>     the type constraints in logics and programming languages.  A
>     single relation with type constraints on its arguments, which
>     is called a star graph, is the simplest kind of canonical graph.
>
>  4. Canonical formation rules are a graph grammar for generating
>     all well formed CGs that preserve the type constraints, but they
>     don't necessarily preserve truth.  (For example, the negation
>     of any statement would obey the same type constraints.)
>
>  5. Inference rules for CGs specify additional constraints
>     that preserve truth.
>
>  6. The CG theory does not use the word 'polymorphism', but it
>     supports a very general kind of polymorphism that is necessary
>     for natural language semantics.  The polymorphism used in
>     programming languages is a subset of the CG polymorphism.
>
> For more detail about these topics, see the following paper:
>
>     http://www.jfsowa.com/cg/cg_hbook.pdf
>
> To support this type system in Common Logic, I adopted the
> following approach:
>
>  1. Define an untyped notation, called Core CGIF (Conceptual
>     Graph Interchange Format), which maps directly to the
>     Common Logic model theory.  In effect, the absence of
>     a type label designates the universal type, which imposes
>     no restriction whatever on the domain of quantification.
>
>  2. Then define Extended CGIF by a translation to Core CGIF.
>     Extended CGIF uses the Common Logic mechanism of restricted
>     quantification.  But it does not enforce the constraints
>     of canonical graphs and the canonical formation rules.
>
>  3. The type labels in Extended CGIF, as in the CLIF dialect
>     of Common Logic, can use any monadic relation to restrict
>     the domain of quantification.  There is no assumption of
>     a type hierarchy or any constraints on type signatures.
>
>  4. Points #1, #2, and #3 are specified in the ISO 24707 standard.
>     But the system of canonical graphs and formation rules add
>     the constraints for a type hierarchy and the graph grammar.
>     Those rules can support the derivation of CGs that preserve
>     the type constraints and the static testing of CGs to verify
>     whether the type constraints are satisfied.
>
>  5. The CG theory assumes a partial ordering of types, but it
>     does not require any specific rules or method for determining
>     that partial ordering.  If desired, the techniques used for
>     Description Logics or the techniques of intuitionistic logic
>     could be used to specify the type hierarchy.
>
> This is the method that I used to add a type system to Common Logic,
> but there is no dependency on a graph grammar.  A similar method
> could be adapted to any type system that anybody might prefer
> to add to Common Logic.
>
> Rick cited the Girard-Reynolds Isomorphism as a desirable feature
> for a type hierarchy.  The proof of that isomorphism used something
> they called "second order logic".  However, the only features they
> required to prove the theorem were the ability to quantify over
> types and relations.  They did not require the hierarchy of
> infinities that are usually assumed in "true" second order logic.
> Common Logic is more than adequate to prove that theorem.
>
> Fundamental principle:  The model theoretic semantics for a logic
> must be compatible with the logic used to derive a type hierarchy
> for a typed version of that logic.  Since intuitionistic logic is
> a subset of FOL (in the sense that every theorem of intuitionistic
> logic is also a theorem of FOL), the use of intuitionistic logic
> for specifying the type hierarchy is compatible with Common Logic.
>
> Therefore, the method I outlined for building the CG type system
> on top of Common Logic can be adapted to the kinds of typed logics
> that Rick was asking for.  In particular, intuitionistic logic,
> the Girard-Reynolds Isomorphism, the Description Logic constraints,
> or many other kinds of constraints can be used for a type system
> that is compatible with the semantics of Common Logic.
>
> John
>
> _________________________________________________________________
> Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
> Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
> Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
> Shared Files: http://ontolog.cim3.net/file/
> Community Wiki: http://ontolog.cim3.net/wiki/
> To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
_________________________________________________________________
To Post: mailto:ontolog-admin@xxxxxxxxxxxxxxxx
Message Archives: http://ontolog.cim3.net/forum/ontolog-admin/
Community Wiki: http://ontolog.cim3.net/wiki/
Shared Files: http://ontolog.cim3.net/file/  
Community Portal: http://ontolog.cim3.net/    (010)
<Prev in Thread] Current Thread [Next in Thread>
  • Re: [ontolog-admin] [ontolog-forum] Type Systems for Common Logic, Peter Yim <=