Abstract:
This paper investigates inference in knowledge bases with fuzzy fuzzy non-Horn facts and rules. Sequent calculi with one structural, one logical rule, and non-logical axioms representing knowledge base rules and facts serve as a proof theory for these knowledge bases. These knowledge bases are also characterized by constrained real-valued models which are applicable to a variety of truth functions. Inference for fuzzy non-Horn knowledge bases is done by applying a variant of ordered resolution, transforming resolution refuations into sequent calculus derivations, building symbolic expressions from the derivations, and evaluating the symbolic expressions.
Key words and phrases:resolution, non-Horn rule, truth function, fuzzy logic, sequent calculus, Reductio Ad Absurdum.