Automated Reasoning Based On Tableaux

History of Automated Theory Proving (ATP) is almost same as that of computer science. It is beginning with ATP about Artificial Intelligence (AI) which is the most advanced field of computer science. As extension of ATP, Automated Reasoning (AR) is basis work of AI. Reasoning system is regarded as the key part in many important AI system. So research of AR will exert a tremendous influence to the other branches of AI. The reasoning methods that rise by AR have been applied widespreadly.Semantic tableau method proposed by Beth (1959) and Hintikka (1955) was introduced to ATP by AI researcher later. Tableau method is virtually show binary relation in semantic structure. In other words properties of binary relation are expressed by logic formulae through introduce corresponding predicate. To different logics the tableau rules are same. It is necessary to extend the structure sets of formulae in order to close corresponding logic system. Computer scientists who were represented by Smullyan and Fitting were interested greatly in tableau method from the 1969's due to its universal and audio-visual properties. It is regarded as another breakthrough after resolution in ATP and one of the important AR. Researchers have been seeking various tableau methods in order to improve efficiency and well-suit for computer implementation. This thesis consists of the following four parts on the basis of tableau.Part One: Tableau methods on classical logics.1. For the quantifier-rule in free variable tableau, since the y-rule requires one to substitute an arbitrary for the quantified variable, which can lead to the y-rule may have to be applied many times to make many free variables have to be showed in tableau proof. On the other hand 8-rule requires Skolem-function symbols are new and all free variables occurring in the current branch are contained. Obviously because y-rule is non-deterministic and 6-rule is limited, an simple proof is become very complexity and tableau close is delay.The modification of 8-rule in [49] is called rules. It is not satisfactory for tableau that occur a lot of free variables. On the basis of 8-rules, we present 8++-rules improved by 8+ -rules and prove its soundness and complete. To apply 8++-rules to TableauTAP system, the result shows 8 +-rules make the tableau close early and improve greatly in time efficiency and space efficiency of deduction.2. In implementing tableaux it is very important for us to limit the number of y-rule applications. The number that y-rule applications affect directly efficiency of tableau. This paper presents a method for recognizing y formulae and introduces an improved algorithm for tableau with y formulae. We have implemented the system -UniTAP by PROLOG. Experimental comparisons have been done between UniTAP and leanTAP software package which is a complete and sound theorem prover for classical first-order logic based on free variable tableaux. By the analyses of 20 of Pelletier's Problems, the results show that the instantiations of variables w.r.t. which the formulae used to close a branch are y formulae are not taken into consideration. This can be taken advantage of to yield shorter tableau Proofs, and in most cases reduced the search space.Part two: Tableau methods on many-valued logics.3. Tableau method with quantifiers in first-order many-valued logic exist uniform expansion rules, and sound and complete have been proved by Zabel and so on. But It is difficulty for computer to implement. Because the number of the branch which have been extended is very large. A Boolean pruning method is proposed in this paper. Tableau rules for such quantifiers can been simplified by providing a link between signed formulas and upset/downset in Boolean set lattices. In addition, through analyzing to Boolean pruning method, we have founded a simplified tableau reasoning method for regular formulas in first-order many-valued logic formulas. It is allowable for us to apply the same extension rules.4. we present a transformation of formulae from arbitrary many-valued l...