Intuitionistic basis for non-monotonic logic

Abstract

McDermott and Doyle [4] suggested a system, denoted by ⊢, of non-monotonic logic. This notion was intended to formalise non-monotonic reasoning as involved in real situations and in artificial intelligence. McDermott and Doyle also list in their paper several difficulties and problems in their approach. Their semantics seems to be inadequate and there are several counterintuitive results obtained in their system.

McDermott and Doyle base their provability notion ⊢ on the provability notion ⊢ of classical logic. We introduce in this note two logical systems based on the provability notion ⊩ of intuitionistic logic. We show that in the resulting nonmonotonic logic most of the problems disappear. We further show that intuitionistic ⊩ is indeed the reasoning adopted implicitly by available TMS (Truth Maintainance Systems).