Research On The Reasoning Methods Using The Extension Rule

Automated reasoning is one of the most important part in artificial intelligence,whose core is reasoning method.As a “complementary” reasoning method with resolution,the research of the extension rule has been widely recognized in the world.As a new rule in automated reasoning,it has unique advantages in some aspects.Nowadays,the main research on the extension rule is among the aspects of complete reasoning methods in propositional logic,incomplete reasoning in propositional logic and complete reasoning in non-classical logic are its short board.This paper designs the framework of incomplete reasoning in propositional logic for the extension rule.And furthermore,this paper applies the extension rule to the reasoning of propositional modal logic S5.Lots of problems in automated reasoning can be converted into SAT solving,local search has much acceleration in algorithms for SAT solving owing to the greedy mode and diversification mode,this paper will combine local search with the extension rule.Owing to the unintelligent transform mode of maximum term,the scale of formulae it can handle are still very small.In this paper,the concept of “maximum term” in logic is utilized,which aimed at designing and implementing the framework of the reasoning for the extension rule based on local search after analysing the relevance of the extension rule and local search.To make the searching process of maximum term more suitable for the framework,a two-mode stochastic local search based on accurately configuration checking and double-sided semi-extension rule is proposed,which is called ERACC(Extension Rule based on Accurately Configuration Checking).After complete the reasoning for the extension rule in propositional logic,this paper applies the extension rule to propositional modal logic S5.According to Kripke semantic model and part of the axioms in S5 system,this paper proposes an NER-based algorithm called PPMCRNER(Parallel Propositional Modal Clausal Reasoning based on Novel Ex-tension Rule)which is used to reason for standard modal clauses in propositional modal logic S5 and has many comparsions with serial version.Algorithms proposed in this paper have good performance in propositional logic and modal logic,which are more excellent than the algorithms based on the extension rule proposed before.ERACC gets much improved in the ability of processing formulae of large scale.This framework makes the extension rule no longer restricted by the scale of formula,and it can also be used in the field of knowledge compilation and possibilistic reasoning.PPMCRNER has good speedup on unsatisfiable clause sets,and it provides a feasible scheme for further research on the reasoning methods for modal formulae which are hard to solve.