An annotated logic theorem prover for an extended possibilistic logic

In this paper we present a theorem prover for possibilistic logic extended with fuzzy constants and fuzzily restricted quantifiers. First of all, we propose a representation for this logic in terms of Horn clauses. We then show how to transform this Horn clause formalism into the generalized annotated logic formalism proposed by Kifer and Subrahmanian in 1992. Specifically, the valuation in a possibilistic clause generates the annotation which will be attached to the head of the annotated clause. We also show how the inference rules of this possibilistic logic can be translated in terms of the mechanisms provided by this annotated logic. Finally, we discuss the implementation of a theorem prover for this possibilistic logic, now translated to annotated logic, in system KOMET, a large-purpose system which has generalized annotated logic as its underlying framework. In this paper we also present proofs relative to the theoretical issues and some examples implemented in KOMET.