Reasoning without Believing: On the Mechanization of Presuppositions and Partiality

Autor: Manfred Kerber and Michael Kohlhase

Herausgeber: Lopez and Mandahar and Nutts

It is well-known that many relevant aspects of everyday reasoning based on natural language cannot be adequately expressed in classical first-order logic. In this paper we address two of the problems, firstly that of so-called presuppositions, expressions from which it is possible to draw implicit conclusion, which classical logic normally does not warrant, and secondly the related problem of partiality and the adequate treatment of undefined expressions. In natural language, presuppositions are quite common, they can, however, only insufficiently be modeled in classical first-order logic. For instance, in the case of universal quantification one normally uses restrictions in natural language and presupposes that these restrictions are non-empty, while in classical logic it is only assumed that the whole universe is non-empty. On the other hand, all constants mentioned in classical logic are presupposed to exist, while it makes no problems to speak about hypothetical objects in everyday language. Similarly, undefined expressions can be handled in natural language discourses and utterances are not only classified into the two categories `true' and `false'. This has led to the development of various better-suited many-valued logics. By combining different approaches we can now give a static description of presuppositions and undefinedness within the same framework. Additionally, we have developed an efficient mechanization of the induced consequence relation (which has been missing in the literature) by combining methods from many-valued truth-functional logics and sort techniques developed for search control in automated theorem proving.