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

[Norbert E. Fuchs]

I have been developing the first-order reasoner RACE [1] for Attempto Controlled English ACE [2] that allows users to check the consistency of a set of ACE axioms, to deduce ACE theorems from ACE axioms and to answer ACE queries from ACE axioms.

RACE uses a set of auxiliary axioms to express context-independent knowledge like the relation between plural nouns and singular nouns, or the ordering relations of natural numbers. These auxiliary axioms are written in Prolog that – having the power of the Turing machine – allows us to practically do any deduction. Thus often the question is not "Is this deduction correct?", but "Should RACE allow for this deduction?".

In the following I would like to discuss a case where this question arises.

Using the power of Prolog I have extended RACE by auxiliary axioms that perform second-order deductions, concretely aggregation. Thus RACE can deduce

  John is a man. Johnny is a man. ⊢ There are two men.

Adding a further axiom establishing that, in fact, Johnny is John, RACE fails.

  John is a man. Johnny is a man. Johnny is John. ⊬ There are two men.

Thus I have a case of non-monotonic reasoning. (Note that RACE can still deduce that there is one man.)

My question to the community is "Should RACE allow for non-monotonic reasoning, or does non-monotonicity have consequences that could confuse RACE users in more complex cases?"

[1] http://attempto.ifi.uzh.ch/race/

[2] http://attempto.ifi.uzh.ch/site/resources/


Norbert E. Fuchs
Department of Informatics & Institute of Computational Linguistics
University of Zurich