On instance defined for non-source sort -- current ALM definitions

[zhangyuanlin]

Several pre-model will be produced. Proposition 1 can be generalized (to non-complete situation) with P_M defined as below

Description of P_M: 
For any link from o to N (non-source node), o not linking to anything below N, 
Let L1 to Lk be leaves of node N, add to PM 

is_a(o, L1) or ... or is_a(o, Lk).

[zhangyuanlin]

A letter to michael to clarify instance and is_a

Michael,

 

This is about our earlier discussion on the understand of instance definition in ALM structure.

 

The ALM structure is to define a pre-model. We tried to make this definition explicit.

Here is your proposal (using example):

 

for any instance definition

  a in S

we have

  instance(a, S).              ---------------------(1)

 

Then the BAT embedded axioms (equation (8) in ALM paper) can be changed to define is_a using instance:

  is_a(X, S1) :- instance(X, S1), source(S1).  ------------------------ (2)

 

(You mentioned is_a might not be a very interesting relation.)

 

There seems to be some discrepancy between this new understanding and an example in ALM.

 

Consider the professor example in the ALM.

Let the example be P1.

---

Theory

……

sorts declarations

    professor :: person

    assistant; associate; full :: professor

……

 

Structure

 alice in professor

---

 

By the  new understanding (1) and (2), the structure of P1 specifies one

premodel: professor = {alice}, assistant = {}, associate = {}, full = {}.

 

However, the ALM paper says the structure specifies three interpretations:

professor = {alice}, assistant = { alice }, associate = {}, full = {}.

professor = {alice}, assistant = {}, associate = { alice }, full = {}.

professor = {alice}, assistant = {}, associate = {}, full = { alice }.


If (1) and (2) does not work, we can discard (2) but just follow original "requirement of" is_a in the definition of interpretation. 


In fact, by following (1) and is_a in definition of interpretation, our understanding 

of professor and alice example will coincide with that in the paper. 


What do you think? 


Thanks,

YL