The Research On The Extension Rule Based Theorem Proving

Automated theorem proving (ATP) has matured into one of the most advancedareas of computer science. Fields where ATP has been successfully used include logic,mathematics, computer science, engineering, and social science. There are potentiallymany more fields where ATP could be used, including biological sciences, medicine,commerce, etc. Many significant problems have been, and continue to be, solved usingATP. The fields where the most notable successes have been achieved are mathematics,and software generation and verification, protocol verification, and hardwareverification.The usually used deduction methods in ATP include resolution based method,tableau based method, sequent calculus and nature deduction method etc. The traditionalidea used in TP is to try to deduce the empty clause to check the unsatisfiability.Resolution based TP is a paradigm of this idea. But extension rule based TP proceedsinversely to resolution. Namely, extension rule based TP checks the unsatisfiability bydeducing the set of clauses consisting of all the maximum terms. Therefore, it is a newtheorem proving method.The difference between resolution based TP and extension rule based TP isfollowing. Resolution based TP goes this way: Since the empty clause is unsatisfiable,once a set of clauses deduces an empty clause, we can decide that it is unsatisfiable, thededuction method used is resolution;While Extension rule based TP goes this way:The set of all the maximum terms is also unsatisfiable. Once a set of clauses deduces it,we can also decide that it is unsatisfiable, the deduction method used here is calledExtension rule. Extension rule based theorem proving can be considered, in a sense, amethod dual to resolution based theorem proving. It outperforms resolution basedmethod when the complementary factor is relatively high. So it is potentially acomplementary method to resolution based methods.As a new reasoning method, whether or not the extension rule method can beapplied well in ATP rely on the efficiency. Since first order extension rule method isreduced to a series of ground-level satisfiability problems, the behavior ofpropositional extension rule will affect the behavior of first order extension ruledirectly. Thus, it seems the speed of the propositional extension rule is so important.Modal logics play important roles in modern logic and are applied widely. Foryears, modal logics have been applied in areas outside pure logic, such as knowledgerepresentation, logics of programs, computational linguistics and agent based systems.The popularity of modal logic can be attributed to its incredibly simple syntax, itsnatural semantics and decidability. Despite the popularity of propositional modal logicand their pleasant properties a problem in real application is the lack of sophisticatedmodal theorem provers. Moreover, modal logics are good candidates for a formaltheory of agents, it needs many modal theorem proving methods too. Concerning theautomated theorem proving in modal logics, there are approximately two ways atpresent. One method is reasoning about the modal logic by the methods in classicallogic directly, such as modal tableaux methods, modal resolution method. Anothermethod is encoding the modal logic into first-order logic by translation method, andthen we can reason by the sophisticated, state-of-the-art tools that are available and thatcontinue to be developed in the area of first-order theorem proving. The translationmethods include relational translation, functional translation, etc. To get morereasoning method for modal logics, it is very necessary to extend the ER method tomodal logics.To speed up the ER method in proposition logic, complete the ER method infirst-order logic, and extend the ER method to modal logics, three aspects work aredone in this thesis.(1) To speed up the ER methods in proposition logic, we improve the algorithmER and IER by few reduction rules and get the extension rule methods with reductionRER and RIER. There are some clauses in the set of clauses having nothing to do withthe satisfiability, such as the clauses containing pure literal, the clauses includingtautology and the clause implied by other clause, etc. Thus, tautology rule, pure literalrule, inclusion rule and single literal rule are used to reduce the given clause set.Meanwhile the unsatisfiability is checked. If the unsatisfiability can be decided duringreduction, it will return the result immediately else return a reduced clause set and callalgorithm ER or IER to check the unsatisfiability of the reduced clause set. Considerthe improved algorithms, when there are no complementary literals at all, it can deducethe satisfiability by using the pure literal rule. Thus it need not invoke the algorithmER or IER which are inefficient in this case. Moreover, by using the single literal ruleto reduce the clause set, it is in fact to use the fast unit resolution to check thesatisfiability. So it is naturally the behavior of algorithms is better than Lin'salgorithms.In algorithm RIER, all clauses which are complementary with clause C aredeleted, so the actual search space are restricted by it. We hope to check thesatisfiability in a space as small as possible so that to improve the efficiency. The sizeof this space is determinative by clause C, so how to select the clause C is very crucial.Based on this fact, we add a heuristic function H for choosing the clause C: In thereduced clause set, we pick the negation of the atom that occurs in the greatest numberof longest clauses into C. The extension rule method with reduction and heuristicHRIER obtain tremendous speed-up, it is the fastest propositional extension rulemethod till now.Though the improved algorithms has no so close relation with complementaryfactory, it is still that the higher the complementary factor of a problem is the moreeffective the improved algorithms are. Namely they are still potentially acomplementary method to resolution based methods. In order to make best use of thetrait of the resolution method and extension rule method, we believe it will get anefficient deduction method by combining them. Direction resolution (DR), the fastestresolution method in proposition logic, is an ordering-based restricted resolution.Algorithm HRIER is the fastest extension rule method in proposition logic till now. Sowe combined DR and HRIER to give a combined reasoning algorithm CDE inproposition logic. The experiment results show the CDE is a fast solver for propositionSAT problems.(2) Reducing the satisfiability methods for first-order logic to a series ofground-level satisfiability problems is more and more attractive. R. Jeroslowintroduced a partial instantiation method of this kind of method. In order to extendJersolsow's work to logic with functions and obtain further speedup, Hooker presentedpartial instantiation methods for inference in first-order logic. unfortunately hisdefinition of blockage is wrong result in his method is incomplete and severalimportant inclusions are not correct. In order to make Hooker's method completeness,we redefine the blockage. Moreover some important theorems are proved under thenew definition.Lin uses the partial instantiation method to promote the extension rule methodfrom propositional logic to first-order logic. But Lin's first-order ER method isincomplete because his definition of potentially blockage is wrong. We give a completefirst-order ER algorithm by revising the definition of potentially blockage. Moreover,we extend the first-order ER with M-satisfiability by giving a bound M, so as to makeit more useful for theorem proving and logic programming (with both definite andindefinite clause). To accelerate the first-order ER, we invoke the improved propositionER method HRIER. The differences between RFOER and Lin's are following. Firstly,the Lin's is incomplete but RFOER is. Secondly, RFOER invokes the algorithmRHIER we have improved, so that it will obtain more speedup. Thirdly, RFOERaugments the case M-satisfiability, and it makes RFOER more flexible and useful inpractice theorem proving.We develop the first-order ER algorithm, a basic practical inference algorithm fornon-Horn first-order logic with functions, and get a first-order theorem prover RFOER.To ensure finite termination of the RFOER algorithm for unsatisfiable formulas, wemodify the procedure by resolving, among the several potentially blockages that mayexits at the same point of time, any one of those having the least nesting depth of themost general unification. By doing this, we ensure that we fully explore the set ofground clauses obtained using constants only upto a certain depth, before proceedingto the next level. Furthermore, the incremental potentially blockage tests technique areused. At last, the prover RFOER are used to solve two kinds of standard andrepresentative planning problem commonly used to study methods of solution ofplanning problems, namely the shortest plan problem and blocks world problem. Theexperiment results show as a basic primal work the behavior and efficiency of proverRFOER is satisfying.(3) In all of presented modal systems, the idea of context is explicit or implicit invarious systems proposed for modal logics. Different parts of a formula can be withinthe scopes of different modal operators, and so may not be applicable to the sameworlds. Occurrences of the same literal may not mean the same thing in differentcontexts ? within different nestings of modal operators. One solution is destructivemethod, it bases on the following fact. For certain modal logics only one context at atime needed to be considered, and when one shifted to a new context details about theold one could be forgotten. It is called destructive method because it loosesinformation during a context shift. Logics amenable to such treatment tend to be thoseKripke models do not involve symmetry ? models that do not permit going back toearlier worlds. We extend the ER method to modal logics by destructive approach. Thedestructive ER method in modal logic K is discussed detailed and those in modalsystems T, K4, S4 and S5 are discussed simply. The destructive ER algorithm DMKERin K is developed and used to solve all of the axioms and four kinds of benchmarkproblems in modal logic K. The experiment results show DMKER is an effectivemodal theorem prover in modal logic K.The semantics-based relational encoding is fairly simple and most straightforward.The prototypical example for the relational translation is propositional uni-modal logic.The relational translation of modal logics imitates their relational semantics. Wepresent the relation extension rule method by extend the ER approach to modal logicsby relation encoding. The method works for those complete and first-order definablemodal logics, which can be characterized by first-order definable class of frames.Function encoding introduces notation for context by world paths. It can encodemore modal information so that provide a considerable improvement of the behavior offirst-order theorem provers on translated non-classical formulae. Because it uses theprefix-stable world path, the first-order formula translated by function encodedapproach needs the special unification algorithm, syntax unification algorithm. Weextend the ER method to modal logics by functional encoding approach to give afunctional ER method in serial modal logics. The functional extension rule methodMFER works for first-order modal logics with constant-domain Kripke semanticswhere the accessibility relation is serial and may have any combination of thefollowing properties: reflexivity, symmetry, transitivity. For the formulae in thenon-serial modal logics, we can use the reasoning approach in serial modal logics tosolve them by setting up a corresponding form non-serial to serial modal logic. Thereexits such correspond, the non-serial modal logics can be translated into serial modallogics adjoined with a special propositional variable de. Based on such translation andalgorithm MFER, we present a generalized functional ER method GMFER innon-serial modal logics.In conclusion, the achievements of this thesis improve and develop the extensionrule based theorem proving method. It has a certain theory significance and applicationimportance. It provides effective methods and means for the research on the reasoningapproach method about ATP in classical and non-classical logic.