- We need instance for non-source sorts in structure
Example 1 (monkey banana problem)
release :: actions
attributes
releaser : agents
released_thing : things
We don't want to make release an instance of every leaf node of actions.
- We use the alice-professor example to illustrate two different opinions
Theory
……
sorts declarations
professor :: person
assistant; associate; full :: professor
……
Structure
alice in professor
2.1 Opinion 1 (from ALM paper)
The example has three pre-models:
professor = {alice}, assistant = { alice }, associate = {}, full = {}.
professor = {alice}, assistant = {}, associate = { alice }, full = {}.
professor = {alice}, assistant = {}, associate = {}, full = { alice }.
2.2 Opinion 2
The example has only one pre-model
professor = {alice}, assistant = { alice }, associate = {}, full = {}.
professor = {alice}, assistant = {}, associate = { alice }, full = {}.
professor = {alice}, assistant = {}, associate = {}, full = { alice }.
We don't want to make release an instance of every leaf node of actions.
2.1 Opinion 1 (from ALM paper)
2.2 Opinion 2