An Improved Method of δ-Rule in Free Variable Semantic Tableau

Automated deduction is always one of the important research topics in AI fields. In recent years the tableau method has been attracting AI researchers’ attention because of its universal and audio-visual properties. Speaking of the quantifier-rule in free variable tableau,the γ -rule requires one to substitute an arbitrary for the quantified variable,which can lead to the γ -rule to be applied many times to make many free variables appear in tableau proof. This paper is aimed at solving the problem that tableau is delayed by free variables that appeared many time in tableau. On the basis of δ +-rule,δ ++ -rule is presented,which is improved by δ +-rule and its soundness is proved. After applying δ ++ -rule to TableauTAP system,the result shows that δ ++ -rule can make the tableau close early and improve greatly in time efficiency and space efficiency of deduction.