(α, β)-Ordered linear resolution of intuitionistic fuzzy propositional logic

This paper presents an approach for (α, β)-resolution-based automated reasoning in intuitionistic fuzzy propositional logic (IFL). In IFL systems, every IFL formula with both a truth degree and a falsity degree at the same time can be transformed into IFL generalized clause based on some equivalent properties in a finite time. With assumed thresholds (α, β), we judge whether each IFL literal of IFL generalized clauses is (α, β)-satisfiable or not. According to the IFL literal's satisfiability, the IFL literals can be divided into two classes, i.e. (α, β)-similar literals and (α, β)-complementary literals. We use the structure of the linear resolution which only has a center line and a side line to restrict the resolution clauses in every resolution procedure. IFL framed literals, recording information of resolved literals instead of storing them in a memory, can be used to reduce the number of possible resolutions and improve the efficiency of the resolution. The empty clause can be obtained with layer resolution where the threshold (α, β) can be changed. The soundness and completeness of (α, β)-ordered linear resolution are proved and an illustrative example is given to verify the (α, β)-ordered linear resolution algorithm and demonstrate its effectiveness.