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.
|