The Existential Entailment Algorithm of β-Problem Solver Markup Language

Problem Solver Markup Language constructed by combining OWL and Horn clauses are studied. The existential entailment algorithm for the decidable description logic is described. In a nonrecursive case,it is shown that a single step of applying a Horn clause needs to be replaced by a more sophisticated reasoning step in β-PSML. This step is isolated and referred to as existential entailment. The existential entailment problem is to decide whether the antecedent of a Horn clause,together with a description logic terminology,logically entail the disjunction of the antecedents of a set of Horn clauses.