Open zhangyuanlin opened 5 years ago
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
Several pre-model will be produced. Proposition 1 can be generalized (to non-complete situation) with P_M defined as below