Reflexivity is an unconventional property for an IS-A **hierarchy. It is**
included here because it helps keeping the number of inference schemes low (note that in the ASP translation we do not need reflexivity).

W **is supposed to include (whether explicitly or via inference) all the**
implications induced by the ontological atoms. For example, if Heard loud bell →IS−A Heard bell is in O **then**
Heard loud bell → Heard bell **is in** W.

Similarly, W **is supposed to include all conditionals induced by the causal**
statements in C. For example, if Flu causes F ever T emperature **is in** C,
then Flu → F ever T emperature **is in** W.

## 2.2 The Formal System

The above ideas are embedded in a short proof system extending classical logic:
1. Causal atoms entail implication: (**α causes β**) → (α → β).

## 2. **Ontological Atoms**

(a) entail implication: If β →IS−A γ **then** β → γ.

(b) transitivity: If α →IS−A β and β →IS−A γ **then** α →IS−A γ.

(c) reflexivity: α →IS−A α

## 3. **Generating The Explanation Atoms**

(a) *Initial case* If δ →IS−A β, δ →IS−A γ, and W 6|= ¬(α ∧ δ),
then (**α causes β**) → α expl γ bec *poss* {**α, δ**}
(b) *Transitivity (gathering the conditions)* If W 6|= ¬V(Φ ∪ Ψ),
then (α expl β bec poss Φ ∧ β expl γ bec *poss* Ψ)
→ α expl γ bec *poss* (Φ ∪ Ψ).

(c) *Simplification of the set of conditions* If W |=VΦ →Wn i=1 VΦi, then Vi∈{1,···,n} α expl β bec poss (Φi∪Φ) → α expl β bec *poss* Φ.

These schemes allow us to obtain the inference patterns evoked in the previous section: