Reasoning without believing: on the mechanisation of presuppositions and partiality.

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-calledpresuppositions, expressions from which it is possible to draw implicit conclusions, which classical logic normally does not warrant, and secondly the problem ofpartialityand the adequate treatment of undefined expressions. In natural language, presuppositions are quite common; however, they cannot be sufficiently modelled in classical first-order logic. For instance, in the case of universal restricted quantification in natural language it is typically presupposed that these restrictions are non-empty, whereas in classical logic it is only assumed that the whole universe is non-empty. Conversely, all constants mentioned in classical logic are presupposed to denote something, while it creates 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 astaticdescription of presuppositions and undefinedness within the same framework. Additionally, we have developed an efficient mechanisation of the induced consequence relation by combining methods from many-valued truth-functional logics and sort techniques developed for search control in automated theorem proving. [ABSTRACT FROM AUTHOR]