Dear John, (01)
OK. Well this looks like model theory stuff, which I largely stopped
worrying about once I realised that if I had a valid instantiated database,
I had a model of my theory. (02)
That is not what I was expecting when I read this in Ali's note: (03)
Quote
Now I know that I went through this really quickly. Some clarifications on
terminology, when I say O1 mapped into entry Rep_O_2, *mapped* means one of
(but not limited to):
. Relative Interpretation
. Faithful Interpretation
. Definable Equivalence
Unquote (04)
MW: I was anticipating that this was about how you map between theories, so
if I have a 3D theory and a 4D theory, and I have some model of the 3D
theory, how do I translate it into an equivalent model of the 4D theory, and
what if any differences are there in what I can infer from the different
theories. (05)
What I can see is that there are at least 3 possibilities: (06)
1. There is a bidirectional mapping such that anything that can be deduced
from one theory is equivalent to something that can be deduced from the
other. You might expect this sort of situation where there is a choice of
which things to take as primitives, and which concepts to define in two
theories of the same thing. (07)
2. Every instance in one theory can be mapped to an instance in the other
theory, but not vice-versa. This is likely when one theory is a
simplification of another theory. (08)
3. Some instances of one theory can be mapped to some instances of another
theory. The usual situation in data exchange between database systems. (09)
MW: I think exploring these relationships between different theories for the
same thing is interesting from an ontology perspective, and significant from
a commercial perspective, because data integration is where there are big
opportunities to make money with computational ontology. (010)
Regards (011)
Matthew West
Information Junction
Tel: +44 560 302 3685
Mobile: +44 750 3385279
matthew.west@xxxxxxxxxxxxxxxxxxxxxxxxx
http://www.informationjunction.co.uk/
http://www.matthew-west.org.uk/ (012)
This email originates from Information Junction Ltd. Registered in England
and Wales No. 6632177.
Registered office: 2 Brookside, Meadow Way, Letchworth Garden City,
Hertfordshire, SG6 3JE. (013)
> -----Original Message-----
> From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-
> bounces@xxxxxxxxxxxxxxxx] On Behalf Of John F. Sowa
> Sent: 23 February 2010 03:36
> To: [ontolog-forum]
> Subject: Re: [ontolog-forum] Semantic interoperability, DL's,
> Expressive Logics and "Primitives"
>
> Folks,
>
> In a note to Matthew and Ali, I promised to translate the formal
> terminology in Ali's note to plain English. But I realize that
> the task of mapping all the formal notation to English + ordinary
> programming terminology is nontrivial. Therefore, I'll start by
> explaining one fundamental term: the word 'model'.
>
> That term has many diverse uses, which create a lot of confusion.
> Therefore, I'll use the term 'Tarski-style model' or 'TS model' for
> the kinds of models that are used in discussions of logic. I don't
> deny the value of other uses, but I want to explain TS models.
>
> I also want to explain the distinction between two very important
> ways of using logic:
>
> 1. Theorem proving, which most logicians talk about and most
> programmers rarely, if ever, do.
>
> 2. Model checking, which logicians sometimes talk about, and which
> relational databases do as a matter of course (but with different
> terminology).
>
> Many people (SemWebbers in particular) make the claim that first-order
> logic is inefficient because theorem proving (#1 above) can sometimes
> be undecidable and can sometimes be intractable (take exponential time
> or worse). That is true. But in many important cases, theorem proving
> can take polynomial time or even linear time.
>
> However, the SemWebbers don't talk about model checking, which never
> takes more than polynomial time. And for many very important cases,
> model checking can be done in linear or even logarithmic time.
>
> The DB gang never use the term 'model checking'. But they do it
> under the terms 'constraint checking' and 'query answering'. Both
> of those practices are efficient and widely used applications of FOL.
>
> For this explanation, I'll use examples of SQL with relational
> databases, but I want to emphasize that network DBs are logically
> *identical* in expressive power to table DBs. Any information stored
> in one can be mapped to a logically equivalent form in the other.
> There may be differences in syntax, performance, human factors,
> etc., but the logic and the semantics are identical. Although I'll
> talk about SQL and relational DBs, these principles also hold for
> anything stored in a graph or network form.
>
> To explain the connection between databases and model checking, the
> first step is to make the comparison between a relational DB and
> a Tarski-style model (TS model).
>
> 1. A Tarski-style model for a first-order language L (such as Common
> Logic) consists of a domain D of *individuals* and a set R of
> *relations* over D. The models for Common Logic also include
> a set F of *functions* over D (but some versions of model theory
> lump the functions with the relations in a single set R).
>
> 2. A relational database also has a set D of all the individuals that
> are named by strings in the DB, and a set T of tables, each of
> which consists of a set of rows (or n-tuples) of strings that
> define some n-adic relation. Since all the tables in T are
> finite,
> they can only define finite relations. However, a DB may also
> contain a set VT of *virtual tables*, which are computed instead
> of being stored. Since virtual relations are not stored, they
> can be infinite -- for example, the greater-than relation over
> numbers is trivial to compute, but impossible to store.
>
> The crucial feature of a Tarski-style model M is an evaluation function
> Phi(s,M), where s is any sentence in the logic L and M is any model
> M=(D,R,F) with domain D, relations R, and functions F. The function
> Phi has two possible values:
>
> Phi(s,M) is *true* if the sentence s is true of the TS model M.
>
> Phi(s,M) is *false* if s is false of M.
>
> Note that every relational database has a unique mapping to a TS model:
>
> 1. The domain D of individuals named in the DB maps to the domain D
> of a TS model.
>
> 2. The n-tuples of any table in the DB can be mapped to the n-tuples
> of either a relation in R or a function in F of a TS model.
>
> 3. The n-tuples that are computed by any virtual relation in the DB
> can also be mapped to either a relation in R or a function in F
> of a TS model.
>
> Even more important, the WHERE clause of an SQL query can express
> full first-order logic: it uses the operators AND, OR, NOT, and
> the quantifier EXISTS in all possible combinations. It can
> therefore be mapped to Common Logic or other versions of FOL.
>
> Finally, the methods for evaluating an SQL WHERE clause in terms
> of a relational DB are *exactly equivalent* to Tarski's definition
> of the evaluation function Phi(s,M).
>
> Since Tarski was defining a mathematical system, he didn't worry
> about computational efficiency in his definition. But the methods
> for evaluating an SQL WHERE clause use various optimizations,
> including indexes over the names in various columns of the tables.
> Even without indexing, every sentence s derived from an SQL WHERE
> clause can be evaluated for truth or falsity in at most polynomial
> time (where the exponent of the polynomial is less than or equal
> to the number of quantifiers in the sentence s). With indexing,
> the amount of computation can often be drastically reduced.
>
> Given this mapping, we can distinguish three applications of model
> checking that use a relational DB:
>
> 1. Updates. Any theory expressed in first-order logic can be
> translated to a collection of *constraints* on permissible
> updates to a database. Each update u converts a DB that
> represents a model M to an updated DB that represents a model M'
> in which the new assertion u is true. But before the update u
> is completed, each constraint is checked against the new model M'.
> If any constraint evaluates to *false* then the update is blocked,
> and the DB remains unchanged.
>
> 2. True-false questions. The truth of any statement s in FOL can
> evaluated in terms of a given DB by translating s to an SQL WHERE
> clause. The SELECT clause for the query does not ask for any data
> to be retrieved; it just checks whether the WHERE clause is true.
>
> 3. WH-questions. Any question that begins with 'who', 'what',
> 'when',
> 'where', or 'which' can answered by an SQL query in which the
> SELECT clause requests the data that make the WHERE clause true.
>
> These are applications of model checking to check constraints
> and to answer questions. Both the constraints and the questions
> can use full expressive power of first-order logic.
>
> No matter how complex the FOL statements, the model checking is
> decidable and efficient. In fact, the entire world economy
> depends on these applications of model checking.
>
> For a tutorial on math and logic, including a brief introduction
> to first-order logic and model theory, see
>
> http://www.jfsowa.com/logic/math.htm
>
> Section 6 of this tutorial shows how relations can be mapped
> to graphs. Sections 8 to 10 survey propositional and predicate
> logic. Section 13 surveys model theory.
>
> For further discussion of some of the points discussed in this
> note, see
>
> http://www.jfsowa.com/pubs/fflogic.pdf
> Fads and fallacies about logic
>
> John Sowa
>
>
> _________________________________________________________________
> 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
> (014)
_________________________________________________________________
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 (015)
|