The satisfiability problem in multiple-valued Horn formulae

Testing the satisfiability of propositional Horn formulae is an important problem within artificial intelligence due to its repercussions in rule-based systems. This problem has been widely studied and its linearity has been proved for the classical case. However, nothing has been published to solve the satisfiability of multiple-valued Horn formulae, although it is closely related to deduction in expert systems frameworks (where a certainty degree is attached to each fact and rule). In this paper, we propose several new results. First, we present a calculus for multiple-valued Horn clauses and claim its soundness and completeness. Second, we offer a detailed description of an almost linear algorithm for testing the satisfiability of multiple-valued Horn formulae. Finally, the minimal model, the minimal inconsistent interpretation and the maximal set of consistent clauses are defined and furnished by another algorithm which is almost linear too. This information is particularly helpful when validating a rule-based system with a knowledge base formed by a set of multiple-valued clauses