Some Notes About PI Proving And Theory Of Truth Degrees Of Logic Formulas

Resolution Principle is an important means of automatic proving of theorem. The purpose of the resolving is to prove with resolution principle that the set of the clauses S is unsatisfiable. PI proving is an important type of resolution proving in predicate logic, where P denotes an order of the predicate symbols, and I denotes a specific interpretation. But, as to the definition of PI reasoning, there are some defects in the present documents, which can't guarantee that every resolving is a PI resolving. In the present paper, a new definition of PI reasoning is proposed in order to make up for the drawback, and two simplified proofs of the lemma needed in the proof of the completeness of PI resolving are provided.Early in 1952 Rosser and Turquette proposed the idea of distinguishing reliabilities of formulas in the propositional logic, and this idea was discussed and developed by many scholars from different points of view. After the integrated semantic theory, Professor Wang Guojun proposed the theory of truth degree of formulas in two-valued propositional logic. Later, based on the same idea, Li Jun gave the theory of truth degrees of formulas in many-valued Lukasiewicz propositional logic and canonical sequence logic system. In the present paper, we propose a kind of theory of truth degrees of formulas in 3-valued Godel and Kleene propositional logic system. The above all the theory of truth degrees of formulas are proposed in propositional logic. As to predicate logic, it is much more complex to find a theory of truth degrees of formulas. The paper first considers it in this field. In two-valued predicate logic, we define a kind of relative truth degrees of formulas, then propose the theory of quasi-truth degrees of formulas, thus a kind of possible logic frame is provided for the theory of approximate reasoning in two-valued predicate logic.The main content of the paper runs as follows:In the first chapter, as preparatory knowledge, the paper gives the concept of PI clash, the Davis and Putnam rule, and some correlative notions. Then we point out the defects in the original definition of PI reasoning, and give the revised one. At last, we give two simplified proof for the necessary lemma in order to prove the completeness theorem of PI resolving.