[Attempto] [CNL] Should I allow for non-monotonic reasoning?

[Norbert E. Fuchs]

> On 25 May 2015, at 11:18 , Norbert E. Fuchs <fuchs at ifi.uzh.ch> wrote:
> 
> ... I tried – but until now was not completely successful – to get default reasoning with the help of modality ...

In the meantime I got the following working in my reasoner RACE

  (1) Tweety is a penguin. Every penguin is a bird. Every bird that cannot fly does not fly. No penguin can fly. |/- Tweety flies.

  (2) Tweety is a penguin. Every penguin is a bird. Every bird that cannot fly does not fly. No penguin can fly. |- Tweety does not fly.

In case (2) RACE correctly reports that the proof depends on all four axioms.

To get so far, I had to modify an auxiliary axiom that RACE uses for the processing of modalities. Regression tests showed that most test cases with modality still work correctly, while a few ones involving negated modality (cannot, does not have to) do not. 

Though my approach to non-monotonicity seems viable it needs further attention.

Best regards.

   --- nef