Non-clausal Resolution in Fuzzy Predicate Logic with Evaluated Syntax background and implementation

The presentation deals with the refutational resolution theorem proving system for the Fuzzy Predicate Logic of First-Order (FPL) based on the general (non-clausal) resolution rule. It is based on the Fuzzy Predicate Logic with Evaluated Syntax. There is also presented an unification algorithm handling existentiality without the need of skolemization. Its idea follows from the general resolution with existentiality for the first-order logic. When the prover is constructed it provides the deductive system, where existing resolution strategies and its implementations may be used with some limitations arising from specific properties of the FPL. Additionaly it presents recent advances in implementation of the above mentioned ideas through an experimental application- Fuzzy Predicate Logic GEneralized Resolution Deductive System. The application provides standard breadth-first search algorithm and also originally developed technique DCF (Detection of Consequent Formulas) that is able to significantly reduce the number of produced resolvents. The DCF method make the inference process practically usable since the standard breadth-firs