Inference methods and semantics on or-type knowledge bases

Abstract

Or-type knowledge is information which has some disjunctive conclusions, for example, (A∨B)←C. We often face with this type of knowledge in our everyday lives. There are several problems to deal with such type of knowledge in computer systems. In general, it is difficult to represent the or-type knowledge in Horn logic. In this paper, we extend first order formulas and define the interpretations for them in a three valued logic. According to the discussion, a Horn clause is also extended so as to deal with the or-type knowledge. We show a fixpoint theorem, the soundness and completeness of a resolution.