hide
Free keywords:
-
Abstract:
This paper is an overview of a variety of results,
all centered around a common theme, namely embedding of
non-classical logics into first order logic and resolution
theorem proving.
We present several classes of non-classical logics, many of
which are of great practical relevance in knowledge
representation, which can be translated into tractable and
relatively simple fragments of classical logic.
In this context, we show that refinements of resolution can
often be used successfully for automated theorem proving,
and in many interesting cases yield optimal decision
procedures.
