Automated theorem proving, non-clausal resolution, general resolution, fuzzy logic, uncertain knowledge

The article presents refutational resolution theorem proving system for the Fuzzy Predicate Logic based on the general (non-clausal) resolution rule. The problem of automated reasoning concerning fuzzy logic requires more complex methods in contrast to classical logic. Additionally we present several inference strategies for efficient theorem proving in fuzzy logic based on Detection of Consequent Formulas algorithm. It is possible to combine it with the standard proof search techniques like breadth-first search or linear search.

The article presents refutational resolution theorem proving system for the Fuzzy Predicate Logic based on the general (non-clausal) resolution rule. The problem of automated reasoning concerning fuzzy logic requires more complex methods in contrast to classical logic. Additionally we present several inference strategies for efficient theorem proving in fuzzy logic based on Detection of Consequent Formulas algorithm. It is possible to combine it with the standard proof search techniques like breadth-first search or linear search.