Algorithm of a-resolution Principle Based on An Intermediate Element Lattice-valued Propositional Logic

摘要

In this paper, algorithm of or-resolution principle based on an intermediate element lattice-valued propositional logic IELP (X) is focused. Concretely, some concepts and results related to LIA,LP(X) and IELP(X) is given firstly. Then, the concrete algorithm of resolution based on IELP(X) is presented. It concludes four steps: First, the algorithm of transforming any formula in IELP (X) to a reducible form is given; second, the equivalent or the same-satisfiable transformation is mentioned; Third, method of resolution based on path searching is expounded; Finally, the method of judging if any processed formula is a -false is given.