非表示:
キーワード:
-
要旨:
This thesis studies the optimised functional translation of propositional modal
logics to first-order logic, and first-order resolution as a means for
realising modal reasoning. The optimised functional translation maps modal
logics to a lattice of clausal logics, called path logics. The general
apparatus of inference for path logics is theory resolution. We show that
satisfiability in basic path logic and certain extensions can be decided by
resolution and condensing without requiring additional refinement strategies.
We propose an improved theory unification algorithm for \textit{S4}, and we
present a calculus of ordered $E$-resolution with normalisation. We show also
that some essentially second-order modal logics convert to path logics, which
can be exploited for accomodating inference for modal logics with numerical
quantifiers in a calculus of resolution and simple arithmetic.
