Non-monotonic inference system handling knowledge allowing classified exceptions

We propose a nonmonotonic formalism for knowledge handling allowing exceptions, the Exc-Representation (ER), and its goal-directed proof procedure, the SLD-EXC resolution, for the nonmonotonic inference system, NISE. ER always provides a unique extension, which is a set of conclusions, and makes tractable the membership problem in nonmonotonic reasoning by introducing the conditional facts, and classifying exceptions into two types based on the relationships among rules