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)
|