An Alternative Proof Method for Possibilistic Logic and its Application
  to Terminological Logics
  Possibilistic logic, an extension of first-order logic, deals with
uncertainty that can be estimated in terms of possibility and necessity
measures. Syntactically, this means that a first-order formula is equipped with
a possibility degree or a necessity degree that expresses to what extent the
formula is possibly or necessarily true. Possibilistic resolution yields a
calculus for possibilistic logic which respects the semantics developed for
possibilistic logic. A drawback, which possibilistic resolution inherits from
classical resolution, is that it may not terminate if applied to formulas
belonging to decidable fragments of first-order logic. Therefore we propose an
alternative proof method for possibilistic logic. The main feature of this
method is that it completely abstracts from a concrete calculus but uses as
basic operation a test for classical entailment. We then instantiate
possibilistic logic with a terminological logic, which is a decidable subclass
o f first-order logic but nevertheless much more expressive than propositional
logic. This yields an extension of terminological logics towards the
representation of uncertain knowledge which is satisfactory from a semantic as
well as algorithmic point of view.
