Reasoning without Believing: On the Mechanization of Presuppositions and Partiality
Author: Manfred Kerber and Michael Kohlhase
Editor: Lopez and Mandahar and Nutts
It is wellknown that many relevant aspects of everyday
reasoning based on natural language cannot be adequately expressed
in classical firstorder logic. In this paper we address two of the
problems, firstly that of socalled 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
firstorder logic. For instance, in the case of universal
quantification one normally uses restrictions in natural language
and presupposes that these restrictions are nonempty, while in
classical logic it is only assumed that the whole universe is
nonempty. 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
bettersuited manyvalued 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 manyvalued
truthfunctional logics and sort techniques developed for search
control in automated theorem proving.
