automated theorem proving, non-clausal resolution, general resolution, description logic, fuzzy logic, fuzzy description logic

The article presents refutational resolution theorem proving system for the Fuzzy Description Logic based on the general (non-clausal) resolution rule. There is also presented a unification algorithm handling existentiality without the need of skolemization. This formalism integrates previously created provers for classical description logic and for fuzzy predicate logic. The problem of automated reasoning concerning fuzzy logic requires more complex methods in contrast to classical logic. Presented formalism overcomes the key unsolvable obstacle - clausal normal form generation (in fuzzy logic) - by introduction of generally applicable inference rule (working with general formulas not only clauses).

The article presents refutational resolution theorem proving system for the Fuzzy Description Logic based on the general (non-clausal) resolution rule. There is also presented a unification algorithm handling existentiality without the need of skolemization. This formalism integrates previously created provers for classical description logic and for fuzzy predicate logic. The problem of automated reasoning concerning fuzzy logic requires more complex methods in contrast to classical logic. Presented formalism overcomes the key unsolvable obstacle - clausal normal form generation (in fuzzy logic) - by introduction of generally applicable inference rule (working with general formulas not only clauses).