[Top] [All Lists]

Re: [ontolog-forum] Requirements of computer language semantics

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: "John F. Sowa" <sowa@xxxxxxxxxxx>
Date: Thu, 19 Mar 2009 01:42:36 -0400
Message-id: <49C1DB4C.70106@xxxxxxxxxxx>
Adrian and Dick,    (01)

AW> Actually, you can just construct a model theory for L1 directly.
 > This may of course lead you to modify L1.  But when the model
 > theory is done, you can use it as a gold standard for implementing
 > a reasoner.  That's way easier and less error prone than trying
 > to do the same kind of thing via L1---> L2.    (02)

I agree that defining a model theory for a language is a very useful
step toward designing an inference engine specifically designed for
that language.    (03)

However, all practical languages for DBs and KBs get data from and
send data to systems that use other languages.  Therefore, it is
highly desirable to define mappings to and from various languages.
In particular, if a language is a subset of FOL (as many are), it
is extremely valuable to specify that mapping as a basis for
implementing translators.    (04)

In short, I would say that for any logic-based language L1, it
is desirable to have both a mapping from L1 to other versions
of logic and a model theory explicitly designed for L1.  Which
one is more important depends on the way L1 will be used.    (05)

RHM> I still have the impression that formal model theory is an
 > academic exercise which has little to do with meaning in the
 > real world.  I don't envision doing anything with model theory
 > when I am using mKE to process knowledge representations.    (06)

That statement is wrong in many different ways:    (07)

  1. Model theory at base is nothing more nor less than a
     systematic way of comparing a sentence to the actual
     world (or a model of the world) and checking whether
     the sentence is true or false.  For simple sentences,
     the comparison takes just one step.  For complex
     sentences, it requires a more systematic process of
     breaking down the sentence into its parts, comparing
     each simple part, and then recombining the results.    (08)

  2. For relational database systems, the raw data in the
     collection of tables consists of simple statements
     that are in a one-to-one relationship with some model
     of the world.  The algorithms for evaluating an SQL
     query in terms of that data (or that model) are
     formally equivalent to Tarski's method for evaluating
     the truth value of a sentence in terms of a model.    (09)

  3. I agree with Adrian and Chris M. that there are good
     reasons for using the model theory for a particular
     logic-based language as a basis for designing an
     inference engine for reasoning about statements in
     that language.  (I quibbled with Chris about whether
     it "makes more sense" to define a separate model
     theory or to define a mapping to some language that
     already has a model theoretic semantics.  But I agree
     with Chris and Adrian that a model theory for a
     given language is useful for designing sound inference
     methods for that language -- and proving that those
     methods are indeed sound.)    (010)

Although I recommended a mapping to CL or IKL as the
simplest and quickest way to define the semantics of
mKR, I also believe that it is important for anyone
who is designing or implementing a logic-based
language to have a working knowledge of model theory.    (011)

John    (012)

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-forum@xxxxxxxxxxxxxxxx    (013)

<Prev in Thread] Current Thread [Next in Thread>