Transcript Powerpoint slides

MODEL THEORY FOR DUMMIES
Basic idea is to give a mathematical characterization of a ‘world’ in just enough
detail to assign a meaning to every expression.
MODEL THEORY FOR DUMMIES
Basic idea is to give a mathematical characterization of a ‘world’ in just enough
detail to assign a meaning to every expression.
Exactly what counts as ‘just enough’ depends on the language.
MODEL THEORY FOR DUMMIES
Basic idea is to give a mathematical characterization of a ‘world’ in just enough detail to assign a
meaning to every expression.
Exactly what counts as ‘just enough’ depends on the language.
Eg. for propositional logic, all you need to know is the truthvalues of the proposition letters, so
an interpretation (“possible world”) is a truth-assignment to the proposition letters.
MODEL THEORY FOR DUMMIES
Basic idea is to give a mathematical characterization of a ‘world’ in just enough detail to assign a
meaning to every expression.
Exactly what counts as ‘just enough’ depends on the language.
Eg. for propositional logic, all you need to know is the truthvalues of the proposition letters, so
an interpretation (“possible world”) is a truth-assignment to the proposition letters.
For first-order logic, you need to know
1.what the quantifiers range over (the universe);
2.for each name, what thing it names;
3.for each relation symbol, what combinations of things make it true (a set of n-tuples).
MODEL THEORY FOR DUMMIES
Basic idea is to give a mathematical characterization of a ‘world’ in just enough detail to assign a
meaning to every expression.
Exactly what counts as ‘just enough’ depends on the language.
Eg. for propositional logic, all you need to know is the truthvalues of the proposition letters, so
an interpretation (“possible world”) is a truth-assignment to the proposition letters.
For first-order logic, you need to know
1.what the quantifiers range over (the universe);
2.for each name, what thing it names;
3.for each relation symbol, what combinations of things make it true (a set of n-tuples).
For maps, you need to know the topological structure of the terrain, the projection function, and
for each map symbol, what property of the terrain region it indicates.
MODEL THEORY FOR DUMMIES
Basic idea is to give a mathematical characterization of a ‘world’ in just enough detail to assign a
meaning to every expression. Exactly what counts as ‘just enough’ depends on the language.
Key point is that MT makes only the assumptions about The World that are needed to determine
truthvalues, and they must be expressible mathematically, ie ‘structurally’. Model theory is
metaphysically neutral. - eg first-order MT doesn’t claim that relations *are* sets of n-tuples;
it just says: whatever relations *really are*, all I need to know about them is which n-tuples they
are true of.
MODEL THEORY FOR DUMMIES
Basic idea is to give a mathematical characterization of a ‘world’ in just enough detail to assign a
meaning to every expression. Exactly what counts as ‘just enough’ depends on the language.
Key point is that MT makes only the assumptions about The World that are needed to determine
truthvalues, and they must be expressible mathematically, ie ‘structurally’. Model theory is
metaphysically neutral
radically agnostic. Eg first-order MT makes no assumptions about what is in the universe.
Basic RDF model theory
An Interpretation is:
0. A set LV and a mapping XL from <qLiteral> to LV
1. A nonempty set IR of resources, called the domain or universe of I.
2. A non-empty subset IP of IR called Properties
3. A mapping IEXT from IP into the powerset of IRx(IR union LV)
4. A mapping IS: vocab(I) -> IR
Basic RDF model theory
An Interpretation is:
0. A set LV and a mapping XL from <qLiteral> to LV
IR could overlap LV
1. A nonempty set IR of resources, called the domain or universe of I.
2. A non-empty subset IP of IR called Properties
3. A mapping IEXT from IP into the powerset of IRx(IR union LV)
4. A mapping IS: vocab(I) -> IR
IS assigns semantic values
to a subset of the total
RDF vocabulary.
i.e. a subset of pairs <x,y>
with x in IR and y in either
IR or LV.
This is basically a table of
the values of this property
for each object. If some
object isn’t mentioned then
it doesn’t have a value for
this property
Basic RDF model theory
An Interpretation is:
0. A set LV and a mapping XL from <qLiteral> to LV
1. A nonempty set IR of resources, called the domain or universe of I.
2. A non-empty subset IP of IR called Properties
3. A mapping IEXT from IP into the powerset of IRx(IR union LV)
4. A mapping IS: vocab(I) -> IR
Which satisfies:
if E is a <uriref> or <anonNode> then I(E) = IS(E)
if E is a <qLiteral> then I(E) = LV(E)
if E is an asserted triple with the form s p o
then I(E) = true iff <I(s),I(o)> is in IEXT(I(p)), otherwise I(E)= false.
if E is a set of triples then I(E) = false just in case I(E') = false for some asserted
triple E' in E, otherwise I(E) = true.
if E is an <ntripleDoc> then I(E) = true if I[A](set(E))=true for some A defined on
anon(E), otherwise I(E)= false
Basic RDF model theory
An Interpretation is:
0. A set LV and a mapping XL from <qLiteral> to LV
1. A nonempty set IR of resources, called the domain or universe of I.
2. A non-empty subset IP of IR called Properties
3. A mapping IEXT from IP into the powerset of IRx(IR union LV)
4. A mapping IS: vocab(I) -> IR
Which satisfies:
if E is a <uriref> or <anonNode> then I(E) = IS(E)
if E is a <qLiteral> then I(E) = LV(E)
This set is probably finite
if E is an asserted triple with the form s p o
then I(E) = true iff <I(s),I(o)> is in IEXT(I(p)), otherwise I(E)= false.
if E is a set of triples then I(E) = false just in case I(E') = false for some asserted
triple E' in E, otherwise I(E) = true.
if E is an <ntripleDoc> then I(E) = true if I[A](set(E))=true for some A defined on
anon(E), otherwise I(E)= false
An example
There are 5 things
in the universe.
vocabulary(I) :
One of
them
doesn’t have
a name
Red
dc:creator
Universe (IR):
Ron
_:someone
_:something
{
IS
IS assigns a value
for each name in the
vocabulary
P
C
}
IEXT
{
P is a property which
assigns values to two
things in the universe.
P
}
IEXT(P) shows what the
values of P are for
everything it is defined on.
An example
There are 5
things in the
universe.
vocabulary(I) :
Red
dc:creator
Universe (IR):
Ron
_:someone
_:something
One of them
doesn’t have a
name
{
IS
{
I( Red dc:creator Ron) = true
P
IEXT
P
C
}
because <I(Red), I(Ron)> is
and
is in IEXT( P ) which is IEXT(I(dc:creator))
I(Red dc:creator _:something) = false
because <I(Red), I(_:something)> is not in
IEXT(I(dc:creator))
[square brackets] are being used to
indicate that this is a document rather
than just a set of triples.
I([Red dc:creator _:something]) = true
because there is a mapping A: _:something
<I(Red), A(_:something)> is in IEXT(I(dc:creator))
and
}
A note on IEXT
It would be simpler to just say that I(p) is a subset of IR x (IR union LV), and write
if E is an asserted triple with the form s p o
then I(E) = true iff <I(s),I(o)> is in I(p), …… rather than IEXT(I(p))…..
Why bother with IEXT?
A note on IEXT
It would be simpler to just say that I(p) is a subset of IR x (IR union LV), and write
if E is an asserted triple with the form s p o
then I(E) = true iff <I(s),I(o)> is in I(p), …… rather than IEXT(I(p))…..
Why bother with IEXT?
Because we might want to interpret a triple like [a a b].
Suppose I(a) was a set of pairs, then how could that set itself be inside one of the pairs in
the set? That would violate the axiom of foundation (a basic axiom of Zermelo-Fraenkel set
theory).
We could use a nonstandard set theory that allows non-well-founded sets, but that would be a
radical move….The use of IEXT is a less controversial alternative.
‘foo’
I
a appears in its own extension, which is fine.
a
IEXT
{<a b> <b b> }
I satisfies E means I(E)=true
E entails E’
means
any I which satisfies E also satisfies E’
Some Lemmas …
1. Any RDF expression has a satisfying interpretation (is consistent). [Herbrand]
2. If I satisfies all the triples in a document, then it satisfies the document.
3. If E and E’ are sets of triples, then E entails E’ iff E contains E’.
4. If E is a document and E’ is an instance of E, then E’ entails E.
5. If E and E’ are documents, then E entails E’ iff there is a set of triples F such that
set(E) contains F and F is an instance of set(E’).
The upshot of 3. and 5. is that all entailments in RDF can be checked by a very simple two-step
process:
E ----take a subset----> F -----existentially generalize---->E’
Skolemization
Replace all anonNodes in a document E by urirefs from a set V (disjoint from vocab(E))
Call this sk(E). Then
1. sk(E) entails E (obviously)
Skolemization
Replace all anonNodes in a document E by urirefs from a set V (disjoin t from vocab(E))
Call this sk(E). Then
1. sk(E) entails E (obviously)
2. E probably doesn’t entail sk(E)
Skolemization
Replace all anonNodes in a document E by urirefs from a set V (disjoin t from vocab(E))
Call this sk(E). Then
1. sk(E) entails E (obviously)
2. E probably doesn’t entail sk(E)
…BUT…
3. If sk(E) entails F and F doesn’t contain any vocabulary from V, then E entails F
Proof: Suppose I satisfies E. Then there is mapping A in anon(E) such that I+A satisfies set(E). If sk(x) is the
uriref that replaces the anonNode x, then define I’ to be like I except I’(sk(x))=A(x), then clearly I’ satisfies
sk(E). sk(E) entails F, so I’ satisfies F, so I’/vocab(F) satisfies F. But vocab(F) does not intersect V, so
I’/vocab(F)=I; whence, I satisfies F. QED.
Skolemization
Replace all anonNodes in a document E by urirefs from a set V (disjoin t from vocab(E))
Call this sk(E). Then
1. sk(E) entails E (obviously)
2. E probably doesn’t entail sk(E)….BUT
3. If sk(E) entails F and F doesn’t contain any vocabulary from V, then E entails F
Proof: Suppose I satisfies E. Then there is mapping A in anon(E) such that I+A satisfies set(E). If sk(x) is the
uriref that replaces the anonNode x, then define I’ to be like I except I’(sk(x))=A(x), then clearly I’ satisifes
sk(E). sk(E) entails F, so I’ satisfies F, so I’/vocab(F) satisfies F. But vocab(F) does not intersect V, so
I’/vocab(F)=I; whence, I satisfies F. QED.
So, as far as V-free expressions are concerned, E and sk(E) entail the same things. So (with the
no-V-provision), asserting sk(E) and asserting E amount to making the same assertion.
Skolemization
Replace all anonNodes in a document E by urirefs from a set V (disjoin t from vocab(E))
Call this sk(E). Then
1. sk(E) entails E (obviously)
2. E probably doesn’t entail sk(E)….BUT
3. If sk(E) entails F and F doesn’t contain any vocabulary from V, then E entails F
Proof: Suppose I satisfies E. Then there is mapping A in anon(E) such that I+A satisfies set(E). If sk(x) is the
uriref that replaces the anonNode x, then define I’ to be like I except I’(sk(x))=A(x), then clearly I’ satisifes
sk(E). sk(E) entails F, so I’ satisfies F, so I’/vocab(F) satisfies F. But vocab(F) does not intersect V, so
I’/vocab(F)=I; whence, I satisfies F. QED.
So, as far as V-free expressions are concerned, E and sk(E) entail the same things. So (with the
no-V-provision), asserting sk(E) and asserting E amount to making the same assertion.
Mind you, it’s different if you aren’t making an assertion…
What does it mean to publish some RDF?
You could be saying:
I am asserting this.
Infer what you like from it.
E entails ????
What does it mean to publish some RDF?
You could be saying:
I am asserting this.
Infer what you like from it.
E entails ????
OR
You could be saying: I am asking about this.
Can you infer it from anything?
???? entails E
What does it mean to publish some RDF?
You could be saying:
I am asserting this.
Infer what you like from it.
E entails ????
OR
You could be saying:
I am asking about this.
Can you infer it from anything?
???? entails E
The model theory works equally well in either case, but the proof techniques differ.
In making an assertion, anonNodes behave very much like urirefs: they both act like logical
constants, and cannot be validly bound to new values at inference time.
In making a query, anonNodes are treated as genuine variables, and can be bound to new
values in order to make inferences possible.
Shared content and relative entailment
?? How do we capture the idea of ‘shared content’ which isn’t explicitly represented in RDF
expressions but on which meaning depends??
Shared content and relative entailment
?? How do we capture the idea of ‘shared content’ which isn’t explicitly represented in RDF
expressions but on which meaning depends??
Idea: express such shared knowledge as mutual acceptance of a set of interpretations which
capture the accepted constraints.
If COM is a set of interpretations, then say that E entails E’ relative to COM if every
interpretation which satisfies E and is compatible with some member of COM also satisfies E’.
Shared content and relative entailment
?? How do we capture the idea of ‘shared content’ which isn’t explicitly represented in RDF
expressions but on which meaning depends??
Idea: express such shared knowledge as mutual acceptance of a set of interpretations which
capture the accepted constraints.
If COM is a set of interpretations, then say that E entails E’ relative to COM if every
interpretation which satisfies E and is compatible with some member of COM also satisfies E’.
COM is an interpretation core. It rules out interpretations which are inconsistent with anything
in COM. Ordinary entailment is entailment relative to { }.
Example: Define an interpretation I with universe the set of possible uri’s starting “http:” , IP = { }, and
IS(x)=the webpage located by Google when given x as input. Then {I} is an interpretation core which represents
an acceptance of Google as a definitive website locator.
Shared content and relative entailment
?? How do we capture the idea of ‘shared content’ which isn’t explicitly represented in RDF
expressions but on which meaning depends??
Idea: express such shared knowledge as mutual acceptance of a set of interpretations which
capture the accepted constraints.
If COM is a set of interpretations, then say that E entails E’ relative to COM if every
interpretation which satisfies E and is compatible with some member of COM also satisfies E’.
COM is an interpretation core. It rules out interpretations which are inconsistent with anything
in COM. Ordinary entailment is entailment relative to { }.
OPEN QUESTIONS
1. How do we specify COM?
2. What properties does relative entailment have? (V. hard to answer in general, but particular
cases might be OK.)
RDFS interpretations
0. A set LV and a mapping XL from <qLiteral> to LV
1. A nonempty set IR of resources, called the domain or universe of I.
2. A non-empty subset IP of IR called Properties
3. A mapping IEXT from IP into the powerset of IRx(IR union LV)
4. A mapping IS: vocab(I) -> IR
5. A nonempty set IC of IR called Classes
6. A mapping ICEXT from IC to the power set of IR union LV
RDFS interpretations
0. A set LV and a mapping XL from <qLiteral> to LV
1. A nonempty set IR of resources, called the domain or universe of I.
2. A non-empty subset IP of IR called Properties
3. A mapping IEXT from IP into the powerset of IRx(IR union LV)
4. A mapping IS: vocab(I) -> IR
5. A nonempty set IC of IR called Classes
6. A mapping ICEXT from IC to the power set of IR union LV
The set of things in the Class
0. A set LV and a mapping XL from <qLiteral> to LV
1. A nonempty set IR of resources, called the domain or universe of I.
2. A non-empty subset IP of IR called Properties
3. A mapping IEXT from IP into the powerset of IRx(IR union LV)
4. A mapping IS: vocab(I) -> IR
5. A nonempty set IC of IR called Classes
6. A mapping ICEXT from IC to the power set of IR union LV
ICEXT(I(rdfs:Resource)) = IR
ICEXT(I(rdf:Property)) = IP
ICEXT(I(rdfs:Class)) = IC
ICEXT(I(rdfs:Literal)) = LV
<x,y> is in IEXT(I(rdf:type)) iff x is in ICEXT(y)
<x,y> is in IEXT(I(rdfs:subClassOf)) iff ICEXT(x) is a subset of ICEXT(y)
<x,y> is in IEXT(rdfs:subPropertyOf)) iff IEXT(x) is a subset of IEXT(y)
I(rdfs:ConstraintResource) is in IC
ICEXT(I(rdfs:ConstraintProperty)) is a subset of the intersection of IP and
ICEXT(I(rdfs:ConstraintResource))
I(rdf:range) and I(rdf:domain) are in ICEXT(I(rdfs:ConstraintProperty))
If <x,y> is in IEXT(I(rdf:range)) and <u,v> is in IEXT(x) then v is in ICEXT(y)
If <x,y> is in IEXT(I(rdf:domain)) and <u,v> is in IEXT(x) then u is in ICEXT(y)
0. A set LV and a mapping XL from <qLiteral> to LV
1. A nonempty set IR of resources, called the domain or universe of I.
2. A non-empty subset IP of IR called Properties
3. A mapping IEXT from IP into the powerset of IRx(IR union LV)
4. A mapping IS: vocab(I) -> IR
5. A nonempty set IC of IR called Classes
6. A mapping ICEXT from IC to the power set of IR union LV
if E is a <uriref> or <anonNode> then I(E) = IS(E)
if E is a <qLiteral> then I(E) = LV(E)
if E is an asserted triple with the form s p o then I(E) = true iff <I(s),I(o)> is in IEXT(I(p)), else I(E)= false.
if E is a set of triples then I(E) = false when I(E') = false for some asserted triple E' in E, else I(E) = true.
if E is an <ntripleDoc> then I(E) = true if I[A](set(E))=true for some A defined on anon(E), else I(E)= false
ICEXT(I(rdfs:Resource)) = IR
ICEXT(I(rdf:Property)) = IP
ICEXT(I(rdfs:Class)) = IC
ICEXT(I(rdfs:Literal)) = LV
<x,y> is in IEXT(I(rdf:type)) iff x is in ICEXT(y)
<x,y> is in IEXT(I(rdfs:subClassOf)) iff ICEXT(x) is a subset of ICEXT(y)
<x,y> is in IEXT(rdfs:subPropertyOf)) iff IEXT(x) is a subset of IEXT(y)
I(rdfs:ConstraintResource) is in IC
ICEXT(I(rdfs:ConstraintProperty)) is a subset of the intersection of IP and ICEXT(I(rdfs:ConstraintResource))
I(rdf:range) and I(rdf:domain) are in ICEXT(I(rdfs:ConstraintProperty))
If <x,y> is in IEXT(I(rdf:range)) and <u,v> is in IEXT(x) then v is in ICEXT(y)
If <x,y> is in IEXT(I(rdf:domain)) and <u,v> is in IEXT(x) then u is in ICEXT(y)
Reification of V
Assume a mapping REIF from V into IR such that:
<x,y> is in IEXT(I(rdf:subject)) iff for some a, b, and c in V, x= REIF(<a b c>) and y= REIF(a)
<x,y> is in IEXT(I(rdf:predicate)) iff for some a, b and c in V, x=REIF(<a b c>) and y= REIF(b)
<x,y> is in IEXT(I(rdf:object)) iff for some a, b and c in V, x=REIF(<a b c>) and y= REIF(c)
x is in ICEXT(I(rdf:Statement)) iff for some a, b and c in V, x=REIF(<a b c>)
Reification of V
Assume a mapping REIF from V into IR such that:
<x,y> is in IEXT(I(rdf:subject)) iff for some a, b, and c in V, x= REIF(<a b c>) and y= REIF(a)
<x,y> is in IEXT(I(rdf:predicate)) iff for some a, b and c in V, x=REIF(<a b c>) and y= REIF(b)
<x,y> is in IEXT(I(rdf:object)) iff for some a, b and c in V, x=REIF(<a b c>) and y= REIF(c)
x is in ICEXT(I(rdf:Statement)) iff for some a, b and c in V, x=REIF(<a b c>)
Syntax
Domain
REIF
Reification of V assuming syntax is in the domain (so REIF is just the identity):
<x,y> is in IEXT(I(rdf:subject)) iff x is a V-triple of the form <y b c>
<x,y> is in IEXT(I(rdf:predicate)) iff x is a V-triple of the form <a y c>
<x,y> is in IEXT(I(rdf:subject)) iff x is a V-triple of the form <a b y>
x is in IEXT(I(rdf:Statement)) iff x is a V-triple.
Reification of V assuming syntax is in the domain (so REIF is just the identity):
<x,y> is in IEXT(I(rdf:subject)) iff x is a V-triple of the form <y b c>
<x,y> is in IEXT(I(rdf:predicate)) iff x is a V-triple of the form <a y c>
<x,y> is in IEXT(I(rdf:subject)) iff x is a V-triple of the form <a b y>
x is in IEXT(I(rdf:Statement)) iff x is a V-triple.
The syntax is in
the domain, so
IEXT isn’t
needed.
Reification of V assuming syntax is in the domain (so REIF is just the identity):
<x,y> is in IEXT(I(rdf:subject)) iff x is a V-triple of the form <y b c>
<x,y> is in IEXT(I(rdf:predicate)) iff x is a V-triple of the form <a y c>
<x,y> is in IEXT(I(rdf:subject)) iff x is a V-triple of the form <a b y>
x is in IEXT(I(rdf:Statement)) iff x is a V-triple.
BUT NOTE there in no way to assert a reified triple, ie to get it interpreted.
(Nothing generates I(<a b c>) )
STILL TO COME
CONTAINERS (alt, aboutEach, aboutEachPrefix) (M&S wording is unclear about and/or)
ABSOLUTE/RELATIVE URIs
SOME METATHEORY LEMMAS FOR RDFS ENTAILMENT