Description:
The article presents refutational resolution theorem proving system for
the Fuzzy Predicate Logic based on the general (non-clausal) resolution
rule. 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.