An Automated Reasoning Expanded Method Based on Set Signs

On the basis of the many-valued logics tableau reasoning, an automated reasoning expansion method based on set sign is presented. This approach which treats set signs as truth values can be applied to some methods and techniques of reasoning suited to classical logics, which make reasoning reform from the non-classical logics to the classical logics. Through rewriting set signs and expansion rules, it is very easy to spread to modal logics, intuitionistic logics and so on. The technology can also be further spread to infinite-valued logic and logic with fuzzy quantifiers(such as T-calculus and S-calculus and so on). The theorem proving system—TSetTAP is implemented by using SWI-PROLOG language in microcomputer. Using method of set signs in the system, rule programming can be generated by only increasing reasoning rules in rule base. System need not be repaired. So some strategies and approaches used in classical logics can easily apply to non-clssical logic. 900 logic questions in TPTP are proved using the system. The result shows TSetTAP makes the tableau close early and improve greatly in time efficiency and space efficiency of reasoning.