Re: Strawman Model Theory

[...]
> > <s> <p> "string" . is true in I if and only if:
> >
> >    s is a member of U, p is a member of P and string is a member of S
> >    (IN(s), IS(string)) is a member of IEXT(I(p))
>
> Just 3 major things missing:
>
> 1. existentials:
>
>    _:x <p> <o> is true in I iff
>    o is a member of U, p is a member of P,
>    and there is some thingy tx in I's set of thingies
>    so that (tx, IN(O)) is a member of IEXT(I(p))
>
>    The substitution (tx for _:x) is
>    said to satisfy the triple _:x <p> <o>.
>
>    In general, a substitution has
>    any number of (thingy for _:name, thingy2 for _:name2, ...)
>    pairs.

I agree and understand 'substitution' as being a mapping from
variables to thingies and usually the identity mapping except
for the given pairs. A substitution denotes bindings of the
variables and instances of the thingies.
A substitution is a unifier of two thingies if the instances
of these thingies by the substitution are identical.
All the rest is just a matter of computing those unifiers and
applying some rules of inference.

> 2. conjunctions
>
>    a list of triples is satisfied by
>    some substitution if each of the triples
>    in it is satisfied by that substitution.

do you mean an (ordered) list or a set?
indeed 'some' substitution is OK
(not a Most General Unifier or MGU)

> 3. putting it all together
>
>    A list of triples is true in I iff there's some
>    substitution that satisfies it.

fine

>
> > Pat goes on to demonstrate a use of this base model theory to
> > define the meaning of reification:
> [...]
> > Pat points out an issue with reification, and I have another,
> > but I suggest we get the base model theory sorted out before we get
> > into that.
>
> Yes, let's leave that for a rainy day...

Well, we had lots of rain here, but that is of course not everywhere...

--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Received on Monday, 23 July 2001 16:35:15 UTC