基于扩展规则的定理证明的研究
|
摘要
自动定理证明自从二十世纪五十年代被提出,已经成为计算机科学中最重要的领域之一。归结方法是其中最著名、应用最广的方法之一。扩展规则方法将定理证明沿着归结的反方向进行,是一种新的定理证明方法。为了使扩展规则方法更好的用于定理证明,本文改进和完善了经典逻辑中的扩展规则定理证明方法,提出了模态逻辑中基于扩展规则的定理证明方法。本文的主要贡献如下:
(1)用化简规则和启发式对命题扩展规则算法进行改进,从而提高命题扩展规则方法的效率。充分利用基于扩展规则方法和基于归结方法的推理特点来提高推理效率,给出了结合这两种推理方法的结合算法。实验结果表明,我们的改进算法大幅度提高了推理效率,特别是带化简规则和启发式函数的扩展规则算法表现得尤为突出。通过把结合算法与相关工作进行比较,可以看出结合算法是一个快速的命题SAT问题求解器。
(2)扩展规则方法是通过部分实例化方法的思想从命题逻辑提升到一阶逻辑的。为了完善Hooker的部分实例化方法,本文重新给出阻塞定义并重新证明了一些定理。为了完善并改进一阶扩展规则算法,本文重新给出潜在阻塞定义,在算法中增加M-可满足的情形,并调用命题逻辑中改进后的扩展规则算法。实现了相应的一阶定理证明器,并用其快速准确的求解了两类非常典型的规划问题。
(3)把扩展规则方法推广到模态典逻辑中。通过破坏性方法直接把扩展规则方法推广到模态逻辑中,主要讨论了模态系统K中的破坏性扩展规则方法。实现了相应的模态定理证明器,用其快速的证明了模态系统K中的所有公理和四类标准的benchmark问题。通过关系转换方法和函数转换方法把扩展规则方法推广到模态逻辑中,提出关系扩展规则方法,函数扩展规则方法和广义函数扩展规则方法。
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 be
applied 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 rule
to 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 effective
modal 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.
(1)用化简规则和启发式对命题扩展规则算法进行改进,从而提高命题扩展规则方法的效率。充分利用基于扩展规则方法和基于归结方法的推理特点来提高推理效率,给出了结合这两种推理方法的结合算法。实验结果表明,我们的改进算法大幅度提高了推理效率,特别是带化简规则和启发式函数的扩展规则算法表现得尤为突出。通过把结合算法与相关工作进行比较,可以看出结合算法是一个快速的命题SAT问题求解器。
(2)扩展规则方法是通过部分实例化方法的思想从命题逻辑提升到一阶逻辑的。为了完善Hooker的部分实例化方法,本文重新给出阻塞定义并重新证明了一些定理。为了完善并改进一阶扩展规则算法,本文重新给出潜在阻塞定义,在算法中增加M-可满足的情形,并调用命题逻辑中改进后的扩展规则算法。实现了相应的一阶定理证明器,并用其快速准确的求解了两类非常典型的规划问题。
(3)把扩展规则方法推广到模态典逻辑中。通过破坏性方法直接把扩展规则方法推广到模态逻辑中,主要讨论了模态系统K中的破坏性扩展规则方法。实现了相应的模态定理证明器,用其快速的证明了模态系统K中的所有公理和四类标准的benchmark问题。通过关系转换方法和函数转换方法把扩展规则方法推广到模态逻辑中,提出关系扩展规则方法,函数扩展规则方法和广义函数扩展规则方法。
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 be
applied 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 rule
to 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 effective
modal 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.
引文
[1] A. Newell, J. C. Shaw, and H. A. Simon. Empirical explorations with the Logic Theory Machine. In: Proc. of West. Joint Comp. Conf., 1957, 218-239. Reproduced in Computers and Thought, McGraw Hill, New York, 1963, 109-133.
[2] H. Gelernter. Empirical explorations of the geometry theorem-proving machine. Computers and Thought, McGraw Hill, New York, 1963, 153-163.
[3] J. R. Slagle. A heuristic program that solves symbolic integration problems in freshman calculus. Computers and Thought, McGraw Hill, New York, 1963, 191-203.
[4] J. McCarthy. Programs with common sense. In Mechanization of Thought Processes (In: Proc. of a symposium held at the National Physics Laboratory) , London, 1959, 77-84.
[5] R. E. Fikes and N. J. Nilsson. STRIPS: A new approach to the application of theorem proving to problem solving. Artificial Intelligence, 1971, 2:189-208.
[6] C. Green. Application of theorem proving to problem solving. In: Proc. of the 1st International Joint Conference on Artificial Intelligence, Washington, D. C., U. S. A.,1969, 219-239.
[7] J. Herbrand. Researches in the theory of demonstration. In J van Heijenoort, editor, From Frege to Goedel: a source book in Mathematical Logic,1879-1931, Harvard University Press, Cambridge, Mass, 1930, 525-581.
[8] P. C. Gilmore. A proof method for quantificational theory, IBM J Res., 1960, 4:28-35.
[9] M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 1960, 7: 201-215.
[10] J. A. Robinson. A machine oriented logic based on the resolution principle. Computer Machine, 1965, 12:23-41.
[11] G. J. Sussman, T. Winograd, and E. Charniak. Micro-planner reference manual. Technical Report203a, M I T AI Lab, 1971.
[12] P. Hayes. In defence of logic. In: Proc. of International Joint Conference on Artificial Intelligence (IJCAI-77), 1977, 559-565.
[13] W. McCune. Solution of the Robbins problem. Journal of Automated Reasoning, 1997, 19(3):263-276.
[14] R. Kowalski. Logic for problem solving. Artificial Intelligence Series. North Holland,1979.
[15] L.C. Paulson. ML for the Working Programmer. Cambridge University Press, 1991.
[16] W. F. Clocksin and C. S. Mellish. Programming in Prolog. Springer Verlag, 1981.
[17] D. Miller and G. Nadathur. An overview of λProlog. In: Proc. of the 5th International Logic Programming Conference/ 5th Symposium on Logic Programming, MIT Press, 1988.
[18] J. Jaffar and M. Maher. Constraint logic programming: A survey. Journal of Logic Programming, 1994, 19/20:503-581.
[19] L. Wos, J. A. Robinson and D. F. Carson. Efficiency and completeness of the set of support strategy in theorem proving. Journal of ACM, 1965, 12(4): 536-541.
[20] J. R. Slagle. Automatic theorem proving with renamable and semantic resolution. Journal of ACM, 1967, 14(4): 23-41.
[21] R. Reiter. Two results on ordering for resolution with merging and linear format. Journal of ACM, 1971, 18(4): 630-646.
[22] D. W. Loveland. A linear format for resolution. In: Proc. of IRIA Symposium on Automatic Demonstration, 1970, 163-190.
[23] R. A. Kowalski and D. Kuehner. Linear resolution with selection function. Artificial Intelligence, 1971, 2:227-260.
[24] C. L. Chang and R. C. T. Lee. Symbolic ogic and mechanical theorem proving. Academic Press, 1973.
[25] 刘叙华,姜云飞. 定理机器证明. 科学出版社, 1987。
[26] R. S. Boyer. Locking: A restriction of resolution. PhD thesis, University of Texas at walski Austin, USA, 1971.
[27] M. E. Stickel. Automated deduction by theory resolution. In: Proc. of the 9th International Joint Conference on Artificial Intelligence, Morgan Kaufmann, Los Angeles, CA, 1985, 1181-1186.
[28] 王湘浩,刘叙华. 广义归结. 计算机学报, 1982, 2: 97-106。
[29] 孙吉贵,刘叙华. 广义线性半锁归结. 科学通报, 1992, 19:1812-1214。
[30] N. V. Murray. Completely nonclausal resolution theorem proving. Artificial Intelligence, 1982, 1:67-85.
[31] G.. Tseitin. [1970], On the complexity of derivation in propositional calculus. Seminars in Mathematics V.A. Steklov Math. Institute, Leningrad, 1970, 8:115-125. Reprinted in Automation of Reasoning, 1983, 2:466-486.
[32] D. Plaisted and S. Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 1986, 2:293-304.
[33] G. A. Robinson and L. Wos. Paramodulation and theorem proving in first order theories with equality. Machine Intelligence, 1969, 4:135-150.
[34] L. Wos and G. A. Robinson. Paramodulation and set of support. In: Proc. of Symposium on Automatic Demonstration, Versailles, France, 1986, 276-310.
[35] C. L. Chang and J. R. Slagle. Completeness of linear resolution for theories with equality. Journal of ACM, 1971, 18(1): 126-136.
[36] R. Anderson. Completeness of the locking restriction for paramodulation. Department of Computer Science, University of Houston, Houston, Texas, 1971.
[37] V. J. Digricoli and M. C. Harison. Equality based binary resolution. Journal of ACM, 1986, 33(2): 253-288.
[38] F. Oppacher and E. Suen. Controlling deduction with proof condensation and heuristics. In: Proc. Of 8th International Conference on Automated Deduction, 1986, 384-393.
[39] M.Moser, O. Ibens, R. Ietz, J. Steinbach, C. Goller, J. Schumann and K. Mayr. SETHEO and E-SETHEO-the CADE-13 systems, Journal of Automated Reasoning, 1997, 18(2): 237-246.
[40] W. Ahrendt, B. Bechkert, R. H?hnle, W. Menzel, W. Relf, G. Schellrorn and P. H. Schmitt. Integration of automated and interactive theorem proving, in W. Bibel and P. Schmitt, eds., Automated Deduction: A Basis for Applications, Kluwer, 1998, Vol. Ⅱ, chapter 4, 97-116.
[41] M. Fitting. First-Order Logic and Automated Theorem Proving. Springer-Verlag, 1990.
[42] P. Andrews. Theorem proving through general matings, Journal of ACM, 1981, 28:193-214.
[43] W. Bible. A comparative study of several proof procedures, Artificial Intelligence, 1982, 18(3): 269-293.
[44] P. Baumgartner, U. Furbach and I. Niemel?. Hyper Tableaux. In: Proc. of European Workshop: Logic in Artificial Intelligence, JELIA, 1996, 1126: 1-17.
[45] P. Baumgartner. Hyper tableau-the next generation. In: Proc. of International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Oosterwijk, The Netherlands, 1998, 60-76.
[46] F. M. Brown. Towards the automation of set theory and its logic. Artificial Intelligence, 1978, 10(3): 281-316.
[47] R. Letz. First-Order Calculi and Proof Procedures for Automated Deduction. PhD thesis, TH Darmstadt, 1993.
[48] B. Beckert. Semantic tableaux with equation. Journal of Logic and Computation, 1997, 7(1): 38-58.
[49] A. Degtyarev. What you always wanted to know about rigid E-unification. Journal of Automated Reasoning, 1998, 20(1): 47-80.
[50] G. Gentzen.Untersuchungen uber das logische Schliessen. Mathematische Zeitschrift, 1935, 39: 176-210 and 405-431. English translation. Investigation into logical deduction, in The Collected Papers of Gerhard Gentzen, M.E.Szabo ed., North-Holland Publishing Co., 1969, 68-131.
[51] M. Davis, G.. Logemann and D. Loveland. A machine program for theorem-proving. Communications of the ACM, 1962, 5(7): 394-397.
[52] M. C. William and W. Larry. Otter -the CADE-13 competition incarnations. Journal of Automated Reasoning, 1997, 18(2): 211-220.
[53] B. Bernhard, H. Reiner, O. Peter and S. Martin. The tableau-based theorem prover: 3TAP Version 4.0. In: Proc. of 13th International Conference on Automated Deduction (CADE 1996), New Brunswick, USA, 1996, 303-307.
[54] K. Sara. Using Isabelle to Prove Simple Theorems. In: Proc. of Higher Order Logic Theorem Proving and its Application, 6th International Workshop (HUG 1993), Vancouver, Canada, 1993, 514-517.
[55] M. Kaufmann and R. S. Boyer. The Boyer-Moore theorem pover and its interative enhancement. Computers and Mathematics with applications, 1995, 19(2): 27-62.
[56] F. Pfenning. Elf: A meta-language for deductive systems. In: Proc. of 12th International Conference on Automated Deduction(CADE 1994), Nancy, France, 1995, 811-815.
[57] P. Michael, M. Smith and J. Rushby. The Enhanced HDM system for specification and verification. ACM Software Engineering Notes, 1985, 10(4):41-43.
[58] I. Horrocks. FaCT and iFaCT. In: Proc. of International Workshop on Description Logics (DL 1999), Link?ping, Sweden, 1999, 133-135.
[59] H. Graham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Journal of Functional Programming, 1994, 4(4): 557-559.
[60] D. F. Jean. An OBJ3 functional specification for boundary representation. Symposium on Solid Modeling and Applications, 1991, 61-72.
[61] S. Victoria. Gordon's Computer: A Hardware Verification Case Study in OBJ3. Formal Methods in System Design, 1994, 4(3): 265-310.
[62] D. R. Smith. KIDS: A Semiautomatic Program Development System. IEEE Transaction of Software Engineering, 1990, 16(9): 1024-1043.
[63] F. Dieter and S. Arno. Using KIV to Specify and Verify Architectures of Knowledge-Based Systems. In: Proc. of International Conference on Automated Software Engineering (ASE 1997), Lake Tahore, CA, USA, 1997, 71-81.
[64] R. Wolfgang. The KIV System: Systematic Construction of Verified Software. In: Proc. of 11th International Conference on Automated Deduction (CADE 1992), NY, USA, 1992, 753-757.
[65] A. Myla. TAME: Using PVS strategies for special-purpose theorem proving. Annals Mathematics and Artificial Intelligence, 2000, 29(1-4): 139-181.
[66] W. Christoph. SPASS -Version 0.49. Journal of Automated Reasoning, 1997, 18(2): 247-252.
[67] S. Kripke. A completeness theorem in modal logic. Journal of Symbolic Logic, 1959, 24:1-14.
[68] D. Gabbay and M. de Rijke, eds., Frontiers of combining systems 2. Studies in Logic and Computation, Research Studies Press/Wiley, 2000.
[69] P. Blackburn and M. de Rijke. Specialissue on combining structures, logics, and Theories. Notre Dame Journal of Formal Logic, 1996, 37.
[70] M. Finger and D. Gabbay. Combining temporal logic systems. Notre Dame Journal of Formal Logic, 1996, 37(2):204-232.
[71] D. Gabbay and V. Shehtman. Products of modal logics, partⅠ . Logic Journal of the IGPL, 1998, 6(1):73-146.
[72] M. Finger and M. Rfynolds. Two-dimensional executable temporal logic for bitemporal databases. Advances in Temporal Logic, 2000, 393-411.
[73] R. Fagin, J. Y. Halpern, Y. Moses and M. Y. Vardi. Reasoning about knowledge. Cambridge, MIT Press, 2003.
[74] M. Wooldridge and N. R. Jennings. Intelligent agents: Theory and practice. The Knowledge Engineering Review, 1995, 10(2): 115-152.
[75] A. S. Rao and M. P. Georgeff. Modeling Agents within a BDI-Architecture. In: Proc. of 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR 1991), Cambridge, MA, USA, 1991, 473-484.
[76] B. van Linder, W. van der Hoek, J. J. Ch. Meyer. How to motivate your agents. Intelligent AgentsⅡ, Springer-Verlag, 1996, 1037: 17-32.
[77] R. C. Moore. A formal theory of knowledge and action. Formal Theories of The Common Sense World, Ablex Publishing, Norwood, NJ, 1985, 319-358.
[78] A.S. Rao. Decision procedures for propositional Linear-Time Belief-Desire-Intention logics. In: Proc. of 14th International Joint Conference on Artificial Intelligence (IJCAI 1995), Workshop on Agent Theories, Architecture, and Language, Montreal, Canada, 1995, 102-118.
[79] W. van der Hoek, B. van Linder and J.J. Ch. Meyer. An integrated modal approach to rational agents. In. Proc. of 2nd AISB Workshop on Practical Reasoning and Rationality, Manchester, UK, 1997, 123-159.
[80] B. Bennett. Logical representations for automated reasoning about spatial relationships. PhD Thesis, University of Leeds, United Kingdom, 1997.
[81] U. Sattler. A concept language extended with different kinds of transitive roles. Deutsche Jahrestagung für Dünstliche Intelligenz, 1996, 333-345.
[82] I. Horrocks. Using an expressive description logic: FaCT or fiction? In: Proc. of 6th International Conference on Principles of Knowledge Representation and Reasoning (KR 1998), Trento, Italy, 1998, 636-647.
[83] D. Calvanese, G. de Giacomo and M. Lenzerini. On the decidability of query containment under constranints. In: Proc. of 7th ACM SIGACT SIGMOD SIGART Symposium on Principles of Database Systems (PODS 1998), Seattle, USA, 1998, 149-158.
[84] D. Calvanese, G. de Giacomo and M. Lenzerini, D. Nardi and R. Rosati. Description Logic Framework for Information Integration. In: Proc. of 6th International Conference on Principles of Knowledge Representation and Reasoning (KR 1998), Trento, Italy, 1998, 2-13.
[85] Rector, A. et al. The GRAIL concept modeling language for medical terminology. Artificial Intelligence in Medicine, 1997, 9:139-171.
[86] I. Horrocks and U. Sattler. A description logic with transitive and inverse roles and role hierarchies. Journal of Logic and Computation, 2000, 9(3): 385-410.
[87] A. Artale and E. Franconi. Temporal description logics. D. Gabby, M. Fisher and L. Vila eds., Handbook of Time and Temporal Reasoning in Artificial Intelligence, MIT Press, 2005.
[88] A. Artale and E. Franconi. A temporal description logic for reasoning about actions and plans. Journal of Artificial Intelligence Research, 1998, 9:463-506.
[89] A. Artale and E. Franconi. Temporal entity-relationship modeling with description logics. In: Proc. of 18th International Conference on Conceptual Modeling (ER 1999), Paris, France, 1999, 81-95.
[90] A. Artale. A temporal description jogic for reasoning over conceptual schemas and queries. In: Proc. of 8th European Conference on Logics in Artificial Intelligence (JELIA 2002), Cosenza, Italy, 2002, 2424: 98-110.
[91] F. Wolter and M. Zakharyaschev. Temporalizing description logics. In: Proc. of 2nd International Workshop on Frontiers of Combining Systems (FroCoS 1998), Amsterdam, Holand, 1998, 379-402.
[92] J.Y. Halpern and Y. Shoham. A propositional modal logic of time intervals. Journal of ACM,1991, 38(4): 935-962.
[93] I. Horrocds. The FaCT system. In: Proc. of International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 1998), Oisterwijk, The Netherlands, 1998, 307-312.
[94] C. Lutz, H. Sturm, F. Wolter and M. Zakhayaschev. Tableaux for temporal description logic with constant domain. In: Proc. of International Joint Conference on Automated Reasoning (IJCAR 2001), Siena, Italy, 2001, 2083: 121-136.
[95] C. Lutz, H. Sturm, F. Wolter and M. Zakhayaschev. Tableau decision algorithm for modalized ALC with constant domains. Studia Logica, 2002, 72(2):199-232.
[96] H. Sturm and F. Wolter. A tableau calculus for temporal description logic: the expanding domain case. Journal of Logic and Computation, 2002, 12 (5): 809-838.
[97] M. Wooldridge, C. Dixon and M. Fisher. A tableau-based proof method for temporal logics of knowledge and belief. Journal of Applied Non-Classical Logics, 1998, 8(3):225-258.
[98] C. Dixon, C. Nalon and M. Fisher. Tableaux for temporal logics of knowledge: synchronous systems of perfect recall or no learning. In: Proc. of 10th International Symposium on Temporal Representation and Reasoning / 4th International Conference on Temporal Logic (TIME-ICTL 2003), Queensland, Australia, 2003, 62-71.
[99] L. N. Nguyen. Analytic tableau systems for propositional bimodal logics of knowledge and belief. In: Proc. of International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2002), Copenhagen, Denmark, 2002, 206-220.
[100] 刘瑞胜, 孙吉贵, 刘叙华. 认识逻辑(1):关于知识和信念的逻辑框架. 计算机学报, 1998, 21(7): 627-637。
[101] 刘瑞胜, 孙吉贵, 刘叙华. 认识逻辑(3):基于语义 tableau 的证明理论. 计算机学报(增刊), 1998, 21: 1-8。
[102] I. Hodkinson, F. Wolter and M. Zakharyaschev. Decidable fragments of first-order temporal logics. Annals of Pure and Applied Logic, 2000, 106:85-134.
[103] R. Kontchakov, I. Hodkinson, F. Wolter and M. Zakharyaschev. Temporalizing Tableaux. Studia Logica, 2004, 76: 91-134.
[104] G. Mints. Gentzen-Type systems and resolution rules, PartⅠ : propositional logic. In: Proc. Of International Conference on Computer Logic, Tallinn, USSR, 1990, 417:198-231.
[105] P. Enjalbert, and L. Farinas del Cerro. Modal resolution in clauset form. Theoretic Computer Science, 1989, 65:1-34.
[106] Y. Auffray, P. Enjalbert and J. Herbrand. Strategies for modal resolution: results and problems. Journal of Automated Reasoning, 1990, 6(1):1-38.
[107] 孙吉贵,刘叙华.。模态归结弱包含删除策略. 计算机学报, 1994, 17(5): 321-329。
[108] 孙吉贵,刘叙华.。标记模态归结推理. 软件学报, 1996, 7(增刊): 156-162。
[109] 孙吉贵,刘叙华. Cialdea 一阶模态归结系统的不完备性及其改进. 计算机学报, 1995, 18(6): 401-408。
[110] 孙吉贵,刘瑞胜,陈荣 标记模态归结推理的推广. 计算机学报, 1999, 2(22): 113-119。
[111] C. Areces, H. de Nivelle and M. de Rijke. Prefixed Resolution: A resolution method for modal and description logics. In: Proc. of 16th International Conference on Automated Deduction (CADE 1999), Trento, Italy, 1999, 187-201.
[112] C. Areces, H. de Nivelle and M. de Rijke. Resolution in modal, description and hybrid logic. Journal of Logic and Computation, 2001, 11(5):717-736.
[113] C. Areces and J. Heguidabehere. HyLoRes: A hybrid logic prover based on direct resolution. In: Proc. of 4th Workshop on Advances in Modal Logic (AIML 2002), Toulouse, France, 2002.
[114] M. Fisher. A resolution method for temporal logic. In: Proc. of 12th International Joint Conference on Artificial Intelligence (IJCAI 1991), Sydney, Australia, 1991, 99-104.
[115] M. Fisher, C. Dixon and M. Peim. Clausal temporal resolution. ACM Transactions on Computational Logic, 2001, 2(1): 12 -56.
[116] C. Dixon M. Fisher and M. Wooldridge. Resolution for temporal kogics of knowledge. Journal of Logic and Computation, 1998, 8(3): 345-372.
[117] A. Degtyarev, M. Fisher and B. Konev. Monodic temporal resolution. In: Proc. of 19th International Conference on Automated Deduction (CADE 2003), Miami, USA, 2003, 2741: 397-411.
[118] B. Konev and A. Degtyarev. Towards the implementation of first-order temporal resolution: the finite domain case. In: Proc. of 10th International Symposium on Temporal Representation and Reasoning / 4th International Conference on Temporal Logic (TIME-ICTL 2003), Queensland, Australia, 2003, 72-82.
[119] B. Konev, A. Degtyarev and M. Fisher. Handling Equality in Monodic Temporal Resolution. In: Proc. of the Logic for Programming and Automated Reasoning (LPAR 2003), Almaty, Kazakhstan, 2003, 2850: 214-228
[120] J. van Benthem. Modal correspondence theory. PhD Thesis, University of Amsterdam, Holand, 1976.
[121] H. J. Ohlbach. Semantics-based translation methods for modal logics. Journal of Logic and Computation, 1991, 1(5): 691-746.
[122] R. A. Schmidt. Optimized modal translation and resolution. PhD Thesis, Universit?t des Saarlandes, 1997.
[123] A. Nonnecgart. A resolution-based calculus for temporal logics. PhD Thesis, Universit?t des Saarlandes, Germany, 1995.
[124] L. Bachmair and H. Ganzinger. A theory of resolution. In: Robinson and A. Voronkov, eds., Handbook of Automated Reasoning, Elsevier Science Publishers, 2001, 19-98.
[125] R.A. Schmidt. Decidability by resolution for prepositional modal logics. Journal of Automated Reasoning, 1999, 22(4): 379-396.
[126] U. Hustadt. Resolution-Based decision procedures for subclasses of first-order logic. PhD Thesis, Universit?t des Saarlandes, Germany, 1999.
[127] U. Hustadt and R.A. Schmidt. On the relation of resolution and tableaux proof systems for description logics. In: Proc. of 16th International Joint Conference on Artificial Intelligence (IJCAI 1999), Stockholm, Sweden, 1999, 110-117.
[128] H. de Nivelle. A resolution decision procedure for the guarded fragment. In: Proc. of 15th International Conference on Automated Deduction (CADE 1998), Lindau, Germany, 1998, 191-204.
[129] C. Christian, G. Fermüller, A. Leitsch, U. Hustadt and T. Tammet. Resolution decision procedures. In: A. Robinson and A. Voronkov, eds., Handbook of Automated Reasoning, Elsevier Science Publishers, 2001, 1791-1849.
[130] U. Hustadt and R.A. Schmidt. Issues of decidability for description logics in the framework of resolution. In: Proc. of Automated Deduction in Classical and Non-Classical Logics (FTP 1998), Vienna, Austria, 1998, 191-205.
[131] U. Hustadt and R.A. Schmidt. Using resolution for testing modal satisfiability and building models. SAT 2000 Special Issue of Journal of Automated Reasoning, 2000, 459-483.
[132] H. Lin, J.G. Sun, Y. M. Zhang. Theorem proving based on extension rule. Journal of Automated Reasoning, Springer, 2003, 31:11-21.
[133] J. N. Hooker,G. Rago, V. Chandru, A. Shrivastava. Partial instantiation methods for inference in first-order Logic. Journal of Automated Reasoning, 2002, 28:371-396.
[134] 刘叙华. 基于归结方法的自动推理. 科学出版社, 北京, 1994。
[135] R. Dechter, I. Rish. Directional resolution: The Davis-Putnam procedure, revisited. In: Proc. of 4th International Conference on Principles of KR&R, Bonn, Germany, 1994, 134-145.
[136] X. Wu, J.G. Sun, S. Lu, M.H. Yin. Propositional Extension Rule with Reduction. International Journal of Computer Science and Network Security, 2006, 6: 190-195.
[137] J. Hooker. Solving the incremental satisfiability problem. Journal of Logic Programming, 1993, 15: 177-186.
[138] J. W. Lloyd. Foundations of logic programming. Springer-Verlag, Berlin, 1987.
[139] H. Ganzinger and K. Korovin. New directions in instantiation-based theorem proving. In: Proc. of 8th Annual IEEE Symposium on Logics in Computer Science (LICS 2003), Ottawa, Canada, 2003, 55-64.
[140] C. Chang and R. C. Lee. Symbolic logic and mechanical theorem proving, Academic Press, 1973.
[141] H. Chu and D.A. Plaisted. Semantically guided first-order theorem proving using hyper-linking. In: Proc. of 12th Conference on Automated Deduction, Nancy, France, 1994, 192-206.
[142] M. Paramasivam and A. D. Plaisted. A replacement rule theorem prover. Journal of Automated Reasoning, 1997, 18:221-226.
[143] R. G. Jeroslow. Computation-oriented reductions of predicate to propositional logic. Decision Support Systems, 1988, 4:183-197.
[144] H. Kautz and B. Selman. Planning as satisfiability. In: Proc. of 10th European Conference on Artificial Intelligence (ECAI 1992), Vienna, Austria, 1992, 359-363.
[145] P. Blachburn, M. Rijke and Y. Venema. Modal logic. Cambridge University Press, 2001.
[146] K. Fine. Normal forms in modal logic. J. Notre Dame ed., Formal Logic, 1975, 16: 229-237. R. Lander. The Computational Complexity of Provability in Systems of Modal Logic. SIAM Journal on Computing, 6:467-480.
[147] H. J. Ohlbach, A. Nonnengart, M. de Rijke and D. M. Gabbay. Encoding tow-valued non-classical logics in classical logic. In: Robinson and A. Voronkov, eds., Handbook of Automated Reasoning, Elsevier Science Publishers, 2001, 1403-1487.
[148] D. M. Gabby. An irreflexivity lemma with applications to axiomatizations of conditions on linear frames. In U. M?nnich, ed., Aspects of Philosophical Logic, Reidel, 1981, 67-89.
[149] R. Ladner. The computational complexity of provability in systems of modal logic. SIAM Journal on Computing, 1977, 6: 467-480.
[150] M. Vardi. Why is modal logic so robustly decidable. In DIMACS Series in Discrete Mathematics and Theoretical Computer Science, AMS, 1997, 149-184.
[151].H. Ganzinger and H. De Niverlle. A superposition decision procedure for the guarded fragment with equality. In: Proc. of 14th IEEE Symposium on Logic in Computer Science (LICS 1999), Trento, Italy, 1999, 295-304.
[152] C. Areces, R. Gennari, J. Heguiabehere and M. De rijke. Tree-based heuristics for modal theorem proving. In: Proc. of 14th European Conference on Artificial Intelligence (ECAI 2000), 2000, 199-203.
[153] H. J. Ohlbach. A resolution calculus for modal logics. In Proc. of 9th International Conference on Automated Deduction (CADE 1988), Argonne, IL, USA, 1988, 500-516.
[154] M. C. Fitting. Destructive modal resolution. Journal of Logic and Computation, 1990, 1:83-97.
[155] M. C. Fitting. Proof methods for modal and intuitionistic logics. D. Reidel Publishing Company, Kruwer, 1983.
[156] L. Fari?as del Cerro and A. Herzig. Linear modal deductions. In Proc. of 9th International Conference on Automated Deduction (CADE 1988), Argonne, IL, USA, 1988, 487-499.
[157] A. Herzig. Raisonnement automatique en Logique modale et algorithms d'unification. PhD thesis, Université, Toulouse, 1989.
[158] N. Zamov. Modal resolution. Soviet Math, 1989, 33: 22-29.
[159] Y. Auffray and P. Enjalbert. Modal theorem proving: An equational viewpoint. Journal of Logic and Computation, 1992, 2(3): 247-297.
[160] J. van Benthem. Beyond accessibility: Functional models for modal logic. In M. de Rijke ed., Diamonds and Defaults, Kluwer, 1993.
[161] D. M. Gabby and H. J. Ohlbach. Quantifier elimination in second-order predicate logic. Journal of South African Computer, 1992, 7: 35-43.
[162] H. J. Ohlbach. Semantic based translation methods for modal logics. Journal of Logic and Computation, 1991, 1(5): 691-746.
[163] H. J. Ohlbach, D. M. Gabby and D. Plaisted. Killer transformations. Research Report MPI-I-94_226, Max-Planck-Institut für Infomatik, Saarbrücken, 1997.
[164] A. Herzig. A new decidable fragment of first order logic. In Abstracts of the 3rd Logical Biennal, Summer School and Conference in Honour of S. C. Kleen, Varna, Bulgaria, 1990.
[165] W. C. Purdy. Decidability of fluted logic with identity. Notre Dame Journal of Formal Logic, 1996, 37(1): 84-104.
[166] W. C. Purdy. Fluted formulas and the limits of decidability. Journal of Symbolic Logic, 1996, 61(2): 608-620.
[167] X. Wu., J.G. Sun, H. Lin and S. S. Feng. Modal extension rule. Process In Natural Science, China, 2005, 15(6): 550-558.
[2] H. Gelernter. Empirical explorations of the geometry theorem-proving machine. Computers and Thought, McGraw Hill, New York, 1963, 153-163.
[3] J. R. Slagle. A heuristic program that solves symbolic integration problems in freshman calculus. Computers and Thought, McGraw Hill, New York, 1963, 191-203.
[4] J. McCarthy. Programs with common sense. In Mechanization of Thought Processes (In: Proc. of a symposium held at the National Physics Laboratory) , London, 1959, 77-84.
[5] R. E. Fikes and N. J. Nilsson. STRIPS: A new approach to the application of theorem proving to problem solving. Artificial Intelligence, 1971, 2:189-208.
[6] C. Green. Application of theorem proving to problem solving. In: Proc. of the 1st International Joint Conference on Artificial Intelligence, Washington, D. C., U. S. A.,1969, 219-239.
[7] J. Herbrand. Researches in the theory of demonstration. In J van Heijenoort, editor, From Frege to Goedel: a source book in Mathematical Logic,1879-1931, Harvard University Press, Cambridge, Mass, 1930, 525-581.
[8] P. C. Gilmore. A proof method for quantificational theory, IBM J Res., 1960, 4:28-35.
[9] M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 1960, 7: 201-215.
[10] J. A. Robinson. A machine oriented logic based on the resolution principle. Computer Machine, 1965, 12:23-41.
[11] G. J. Sussman, T. Winograd, and E. Charniak. Micro-planner reference manual. Technical Report203a, M I T AI Lab, 1971.
[12] P. Hayes. In defence of logic. In: Proc. of International Joint Conference on Artificial Intelligence (IJCAI-77), 1977, 559-565.
[13] W. McCune. Solution of the Robbins problem. Journal of Automated Reasoning, 1997, 19(3):263-276.
[14] R. Kowalski. Logic for problem solving. Artificial Intelligence Series. North Holland,1979.
[15] L.C. Paulson. ML for the Working Programmer. Cambridge University Press, 1991.
[16] W. F. Clocksin and C. S. Mellish. Programming in Prolog. Springer Verlag, 1981.
[17] D. Miller and G. Nadathur. An overview of λProlog. In: Proc. of the 5th International Logic Programming Conference/ 5th Symposium on Logic Programming, MIT Press, 1988.
[18] J. Jaffar and M. Maher. Constraint logic programming: A survey. Journal of Logic Programming, 1994, 19/20:503-581.
[19] L. Wos, J. A. Robinson and D. F. Carson. Efficiency and completeness of the set of support strategy in theorem proving. Journal of ACM, 1965, 12(4): 536-541.
[20] J. R. Slagle. Automatic theorem proving with renamable and semantic resolution. Journal of ACM, 1967, 14(4): 23-41.
[21] R. Reiter. Two results on ordering for resolution with merging and linear format. Journal of ACM, 1971, 18(4): 630-646.
[22] D. W. Loveland. A linear format for resolution. In: Proc. of IRIA Symposium on Automatic Demonstration, 1970, 163-190.
[23] R. A. Kowalski and D. Kuehner. Linear resolution with selection function. Artificial Intelligence, 1971, 2:227-260.
[24] C. L. Chang and R. C. T. Lee. Symbolic ogic and mechanical theorem proving. Academic Press, 1973.
[25] 刘叙华,姜云飞. 定理机器证明. 科学出版社, 1987。
[26] R. S. Boyer. Locking: A restriction of resolution. PhD thesis, University of Texas at walski Austin, USA, 1971.
[27] M. E. Stickel. Automated deduction by theory resolution. In: Proc. of the 9th International Joint Conference on Artificial Intelligence, Morgan Kaufmann, Los Angeles, CA, 1985, 1181-1186.
[28] 王湘浩,刘叙华. 广义归结. 计算机学报, 1982, 2: 97-106。
[29] 孙吉贵,刘叙华. 广义线性半锁归结. 科学通报, 1992, 19:1812-1214。
[30] N. V. Murray. Completely nonclausal resolution theorem proving. Artificial Intelligence, 1982, 1:67-85.
[31] G.. Tseitin. [1970], On the complexity of derivation in propositional calculus. Seminars in Mathematics V.A. Steklov Math. Institute, Leningrad, 1970, 8:115-125. Reprinted in Automation of Reasoning, 1983, 2:466-486.
[32] D. Plaisted and S. Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 1986, 2:293-304.
[33] G. A. Robinson and L. Wos. Paramodulation and theorem proving in first order theories with equality. Machine Intelligence, 1969, 4:135-150.
[34] L. Wos and G. A. Robinson. Paramodulation and set of support. In: Proc. of Symposium on Automatic Demonstration, Versailles, France, 1986, 276-310.
[35] C. L. Chang and J. R. Slagle. Completeness of linear resolution for theories with equality. Journal of ACM, 1971, 18(1): 126-136.
[36] R. Anderson. Completeness of the locking restriction for paramodulation. Department of Computer Science, University of Houston, Houston, Texas, 1971.
[37] V. J. Digricoli and M. C. Harison. Equality based binary resolution. Journal of ACM, 1986, 33(2): 253-288.
[38] F. Oppacher and E. Suen. Controlling deduction with proof condensation and heuristics. In: Proc. Of 8th International Conference on Automated Deduction, 1986, 384-393.
[39] M.Moser, O. Ibens, R. Ietz, J. Steinbach, C. Goller, J. Schumann and K. Mayr. SETHEO and E-SETHEO-the CADE-13 systems, Journal of Automated Reasoning, 1997, 18(2): 237-246.
[40] W. Ahrendt, B. Bechkert, R. H?hnle, W. Menzel, W. Relf, G. Schellrorn and P. H. Schmitt. Integration of automated and interactive theorem proving, in W. Bibel and P. Schmitt, eds., Automated Deduction: A Basis for Applications, Kluwer, 1998, Vol. Ⅱ, chapter 4, 97-116.
[41] M. Fitting. First-Order Logic and Automated Theorem Proving. Springer-Verlag, 1990.
[42] P. Andrews. Theorem proving through general matings, Journal of ACM, 1981, 28:193-214.
[43] W. Bible. A comparative study of several proof procedures, Artificial Intelligence, 1982, 18(3): 269-293.
[44] P. Baumgartner, U. Furbach and I. Niemel?. Hyper Tableaux. In: Proc. of European Workshop: Logic in Artificial Intelligence, JELIA, 1996, 1126: 1-17.
[45] P. Baumgartner. Hyper tableau-the next generation. In: Proc. of International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Oosterwijk, The Netherlands, 1998, 60-76.
[46] F. M. Brown. Towards the automation of set theory and its logic. Artificial Intelligence, 1978, 10(3): 281-316.
[47] R. Letz. First-Order Calculi and Proof Procedures for Automated Deduction. PhD thesis, TH Darmstadt, 1993.
[48] B. Beckert. Semantic tableaux with equation. Journal of Logic and Computation, 1997, 7(1): 38-58.
[49] A. Degtyarev. What you always wanted to know about rigid E-unification. Journal of Automated Reasoning, 1998, 20(1): 47-80.
[50] G. Gentzen.Untersuchungen uber das logische Schliessen. Mathematische Zeitschrift, 1935, 39: 176-210 and 405-431. English translation. Investigation into logical deduction, in The Collected Papers of Gerhard Gentzen, M.E.Szabo ed., North-Holland Publishing Co., 1969, 68-131.
[51] M. Davis, G.. Logemann and D. Loveland. A machine program for theorem-proving. Communications of the ACM, 1962, 5(7): 394-397.
[52] M. C. William and W. Larry. Otter -the CADE-13 competition incarnations. Journal of Automated Reasoning, 1997, 18(2): 211-220.
[53] B. Bernhard, H. Reiner, O. Peter and S. Martin. The tableau-based theorem prover: 3TAP Version 4.0. In: Proc. of 13th International Conference on Automated Deduction (CADE 1996), New Brunswick, USA, 1996, 303-307.
[54] K. Sara. Using Isabelle to Prove Simple Theorems. In: Proc. of Higher Order Logic Theorem Proving and its Application, 6th International Workshop (HUG 1993), Vancouver, Canada, 1993, 514-517.
[55] M. Kaufmann and R. S. Boyer. The Boyer-Moore theorem pover and its interative enhancement. Computers and Mathematics with applications, 1995, 19(2): 27-62.
[56] F. Pfenning. Elf: A meta-language for deductive systems. In: Proc. of 12th International Conference on Automated Deduction(CADE 1994), Nancy, France, 1995, 811-815.
[57] P. Michael, M. Smith and J. Rushby. The Enhanced HDM system for specification and verification. ACM Software Engineering Notes, 1985, 10(4):41-43.
[58] I. Horrocks. FaCT and iFaCT. In: Proc. of International Workshop on Description Logics (DL 1999), Link?ping, Sweden, 1999, 133-135.
[59] H. Graham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Journal of Functional Programming, 1994, 4(4): 557-559.
[60] D. F. Jean. An OBJ3 functional specification for boundary representation. Symposium on Solid Modeling and Applications, 1991, 61-72.
[61] S. Victoria. Gordon's Computer: A Hardware Verification Case Study in OBJ3. Formal Methods in System Design, 1994, 4(3): 265-310.
[62] D. R. Smith. KIDS: A Semiautomatic Program Development System. IEEE Transaction of Software Engineering, 1990, 16(9): 1024-1043.
[63] F. Dieter and S. Arno. Using KIV to Specify and Verify Architectures of Knowledge-Based Systems. In: Proc. of International Conference on Automated Software Engineering (ASE 1997), Lake Tahore, CA, USA, 1997, 71-81.
[64] R. Wolfgang. The KIV System: Systematic Construction of Verified Software. In: Proc. of 11th International Conference on Automated Deduction (CADE 1992), NY, USA, 1992, 753-757.
[65] A. Myla. TAME: Using PVS strategies for special-purpose theorem proving. Annals Mathematics and Artificial Intelligence, 2000, 29(1-4): 139-181.
[66] W. Christoph. SPASS -Version 0.49. Journal of Automated Reasoning, 1997, 18(2): 247-252.
[67] S. Kripke. A completeness theorem in modal logic. Journal of Symbolic Logic, 1959, 24:1-14.
[68] D. Gabbay and M. de Rijke, eds., Frontiers of combining systems 2. Studies in Logic and Computation, Research Studies Press/Wiley, 2000.
[69] P. Blackburn and M. de Rijke. Specialissue on combining structures, logics, and Theories. Notre Dame Journal of Formal Logic, 1996, 37.
[70] M. Finger and D. Gabbay. Combining temporal logic systems. Notre Dame Journal of Formal Logic, 1996, 37(2):204-232.
[71] D. Gabbay and V. Shehtman. Products of modal logics, partⅠ . Logic Journal of the IGPL, 1998, 6(1):73-146.
[72] M. Finger and M. Rfynolds. Two-dimensional executable temporal logic for bitemporal databases. Advances in Temporal Logic, 2000, 393-411.
[73] R. Fagin, J. Y. Halpern, Y. Moses and M. Y. Vardi. Reasoning about knowledge. Cambridge, MIT Press, 2003.
[74] M. Wooldridge and N. R. Jennings. Intelligent agents: Theory and practice. The Knowledge Engineering Review, 1995, 10(2): 115-152.
[75] A. S. Rao and M. P. Georgeff. Modeling Agents within a BDI-Architecture. In: Proc. of 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR 1991), Cambridge, MA, USA, 1991, 473-484.
[76] B. van Linder, W. van der Hoek, J. J. Ch. Meyer. How to motivate your agents. Intelligent AgentsⅡ, Springer-Verlag, 1996, 1037: 17-32.
[77] R. C. Moore. A formal theory of knowledge and action. Formal Theories of The Common Sense World, Ablex Publishing, Norwood, NJ, 1985, 319-358.
[78] A.S. Rao. Decision procedures for propositional Linear-Time Belief-Desire-Intention logics. In: Proc. of 14th International Joint Conference on Artificial Intelligence (IJCAI 1995), Workshop on Agent Theories, Architecture, and Language, Montreal, Canada, 1995, 102-118.
[79] W. van der Hoek, B. van Linder and J.J. Ch. Meyer. An integrated modal approach to rational agents. In. Proc. of 2nd AISB Workshop on Practical Reasoning and Rationality, Manchester, UK, 1997, 123-159.
[80] B. Bennett. Logical representations for automated reasoning about spatial relationships. PhD Thesis, University of Leeds, United Kingdom, 1997.
[81] U. Sattler. A concept language extended with different kinds of transitive roles. Deutsche Jahrestagung für Dünstliche Intelligenz, 1996, 333-345.
[82] I. Horrocks. Using an expressive description logic: FaCT or fiction? In: Proc. of 6th International Conference on Principles of Knowledge Representation and Reasoning (KR 1998), Trento, Italy, 1998, 636-647.
[83] D. Calvanese, G. de Giacomo and M. Lenzerini. On the decidability of query containment under constranints. In: Proc. of 7th ACM SIGACT SIGMOD SIGART Symposium on Principles of Database Systems (PODS 1998), Seattle, USA, 1998, 149-158.
[84] D. Calvanese, G. de Giacomo and M. Lenzerini, D. Nardi and R. Rosati. Description Logic Framework for Information Integration. In: Proc. of 6th International Conference on Principles of Knowledge Representation and Reasoning (KR 1998), Trento, Italy, 1998, 2-13.
[85] Rector, A. et al. The GRAIL concept modeling language for medical terminology. Artificial Intelligence in Medicine, 1997, 9:139-171.
[86] I. Horrocks and U. Sattler. A description logic with transitive and inverse roles and role hierarchies. Journal of Logic and Computation, 2000, 9(3): 385-410.
[87] A. Artale and E. Franconi. Temporal description logics. D. Gabby, M. Fisher and L. Vila eds., Handbook of Time and Temporal Reasoning in Artificial Intelligence, MIT Press, 2005.
[88] A. Artale and E. Franconi. A temporal description logic for reasoning about actions and plans. Journal of Artificial Intelligence Research, 1998, 9:463-506.
[89] A. Artale and E. Franconi. Temporal entity-relationship modeling with description logics. In: Proc. of 18th International Conference on Conceptual Modeling (ER 1999), Paris, France, 1999, 81-95.
[90] A. Artale. A temporal description jogic for reasoning over conceptual schemas and queries. In: Proc. of 8th European Conference on Logics in Artificial Intelligence (JELIA 2002), Cosenza, Italy, 2002, 2424: 98-110.
[91] F. Wolter and M. Zakharyaschev. Temporalizing description logics. In: Proc. of 2nd International Workshop on Frontiers of Combining Systems (FroCoS 1998), Amsterdam, Holand, 1998, 379-402.
[92] J.Y. Halpern and Y. Shoham. A propositional modal logic of time intervals. Journal of ACM,1991, 38(4): 935-962.
[93] I. Horrocds. The FaCT system. In: Proc. of International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 1998), Oisterwijk, The Netherlands, 1998, 307-312.
[94] C. Lutz, H. Sturm, F. Wolter and M. Zakhayaschev. Tableaux for temporal description logic with constant domain. In: Proc. of International Joint Conference on Automated Reasoning (IJCAR 2001), Siena, Italy, 2001, 2083: 121-136.
[95] C. Lutz, H. Sturm, F. Wolter and M. Zakhayaschev. Tableau decision algorithm for modalized ALC with constant domains. Studia Logica, 2002, 72(2):199-232.
[96] H. Sturm and F. Wolter. A tableau calculus for temporal description logic: the expanding domain case. Journal of Logic and Computation, 2002, 12 (5): 809-838.
[97] M. Wooldridge, C. Dixon and M. Fisher. A tableau-based proof method for temporal logics of knowledge and belief. Journal of Applied Non-Classical Logics, 1998, 8(3):225-258.
[98] C. Dixon, C. Nalon and M. Fisher. Tableaux for temporal logics of knowledge: synchronous systems of perfect recall or no learning. In: Proc. of 10th International Symposium on Temporal Representation and Reasoning / 4th International Conference on Temporal Logic (TIME-ICTL 2003), Queensland, Australia, 2003, 62-71.
[99] L. N. Nguyen. Analytic tableau systems for propositional bimodal logics of knowledge and belief. In: Proc. of International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2002), Copenhagen, Denmark, 2002, 206-220.
[100] 刘瑞胜, 孙吉贵, 刘叙华. 认识逻辑(1):关于知识和信念的逻辑框架. 计算机学报, 1998, 21(7): 627-637。
[101] 刘瑞胜, 孙吉贵, 刘叙华. 认识逻辑(3):基于语义 tableau 的证明理论. 计算机学报(增刊), 1998, 21: 1-8。
[102] I. Hodkinson, F. Wolter and M. Zakharyaschev. Decidable fragments of first-order temporal logics. Annals of Pure and Applied Logic, 2000, 106:85-134.
[103] R. Kontchakov, I. Hodkinson, F. Wolter and M. Zakharyaschev. Temporalizing Tableaux. Studia Logica, 2004, 76: 91-134.
[104] G. Mints. Gentzen-Type systems and resolution rules, PartⅠ : propositional logic. In: Proc. Of International Conference on Computer Logic, Tallinn, USSR, 1990, 417:198-231.
[105] P. Enjalbert, and L. Farinas del Cerro. Modal resolution in clauset form. Theoretic Computer Science, 1989, 65:1-34.
[106] Y. Auffray, P. Enjalbert and J. Herbrand. Strategies for modal resolution: results and problems. Journal of Automated Reasoning, 1990, 6(1):1-38.
[107] 孙吉贵,刘叙华.。模态归结弱包含删除策略. 计算机学报, 1994, 17(5): 321-329。
[108] 孙吉贵,刘叙华.。标记模态归结推理. 软件学报, 1996, 7(增刊): 156-162。
[109] 孙吉贵,刘叙华. Cialdea 一阶模态归结系统的不完备性及其改进. 计算机学报, 1995, 18(6): 401-408。
[110] 孙吉贵,刘瑞胜,陈荣 标记模态归结推理的推广. 计算机学报, 1999, 2(22): 113-119。
[111] C. Areces, H. de Nivelle and M. de Rijke. Prefixed Resolution: A resolution method for modal and description logics. In: Proc. of 16th International Conference on Automated Deduction (CADE 1999), Trento, Italy, 1999, 187-201.
[112] C. Areces, H. de Nivelle and M. de Rijke. Resolution in modal, description and hybrid logic. Journal of Logic and Computation, 2001, 11(5):717-736.
[113] C. Areces and J. Heguidabehere. HyLoRes: A hybrid logic prover based on direct resolution. In: Proc. of 4th Workshop on Advances in Modal Logic (AIML 2002), Toulouse, France, 2002.
[114] M. Fisher. A resolution method for temporal logic. In: Proc. of 12th International Joint Conference on Artificial Intelligence (IJCAI 1991), Sydney, Australia, 1991, 99-104.
[115] M. Fisher, C. Dixon and M. Peim. Clausal temporal resolution. ACM Transactions on Computational Logic, 2001, 2(1): 12 -56.
[116] C. Dixon M. Fisher and M. Wooldridge. Resolution for temporal kogics of knowledge. Journal of Logic and Computation, 1998, 8(3): 345-372.
[117] A. Degtyarev, M. Fisher and B. Konev. Monodic temporal resolution. In: Proc. of 19th International Conference on Automated Deduction (CADE 2003), Miami, USA, 2003, 2741: 397-411.
[118] B. Konev and A. Degtyarev. Towards the implementation of first-order temporal resolution: the finite domain case. In: Proc. of 10th International Symposium on Temporal Representation and Reasoning / 4th International Conference on Temporal Logic (TIME-ICTL 2003), Queensland, Australia, 2003, 72-82.
[119] B. Konev, A. Degtyarev and M. Fisher. Handling Equality in Monodic Temporal Resolution. In: Proc. of the Logic for Programming and Automated Reasoning (LPAR 2003), Almaty, Kazakhstan, 2003, 2850: 214-228
[120] J. van Benthem. Modal correspondence theory. PhD Thesis, University of Amsterdam, Holand, 1976.
[121] H. J. Ohlbach. Semantics-based translation methods for modal logics. Journal of Logic and Computation, 1991, 1(5): 691-746.
[122] R. A. Schmidt. Optimized modal translation and resolution. PhD Thesis, Universit?t des Saarlandes, 1997.
[123] A. Nonnecgart. A resolution-based calculus for temporal logics. PhD Thesis, Universit?t des Saarlandes, Germany, 1995.
[124] L. Bachmair and H. Ganzinger. A theory of resolution. In: Robinson and A. Voronkov, eds., Handbook of Automated Reasoning, Elsevier Science Publishers, 2001, 19-98.
[125] R.A. Schmidt. Decidability by resolution for prepositional modal logics. Journal of Automated Reasoning, 1999, 22(4): 379-396.
[126] U. Hustadt. Resolution-Based decision procedures for subclasses of first-order logic. PhD Thesis, Universit?t des Saarlandes, Germany, 1999.
[127] U. Hustadt and R.A. Schmidt. On the relation of resolution and tableaux proof systems for description logics. In: Proc. of 16th International Joint Conference on Artificial Intelligence (IJCAI 1999), Stockholm, Sweden, 1999, 110-117.
[128] H. de Nivelle. A resolution decision procedure for the guarded fragment. In: Proc. of 15th International Conference on Automated Deduction (CADE 1998), Lindau, Germany, 1998, 191-204.
[129] C. Christian, G. Fermüller, A. Leitsch, U. Hustadt and T. Tammet. Resolution decision procedures. In: A. Robinson and A. Voronkov, eds., Handbook of Automated Reasoning, Elsevier Science Publishers, 2001, 1791-1849.
[130] U. Hustadt and R.A. Schmidt. Issues of decidability for description logics in the framework of resolution. In: Proc. of Automated Deduction in Classical and Non-Classical Logics (FTP 1998), Vienna, Austria, 1998, 191-205.
[131] U. Hustadt and R.A. Schmidt. Using resolution for testing modal satisfiability and building models. SAT 2000 Special Issue of Journal of Automated Reasoning, 2000, 459-483.
[132] H. Lin, J.G. Sun, Y. M. Zhang. Theorem proving based on extension rule. Journal of Automated Reasoning, Springer, 2003, 31:11-21.
[133] J. N. Hooker,G. Rago, V. Chandru, A. Shrivastava. Partial instantiation methods for inference in first-order Logic. Journal of Automated Reasoning, 2002, 28:371-396.
[134] 刘叙华. 基于归结方法的自动推理. 科学出版社, 北京, 1994。
[135] R. Dechter, I. Rish. Directional resolution: The Davis-Putnam procedure, revisited. In: Proc. of 4th International Conference on Principles of KR&R, Bonn, Germany, 1994, 134-145.
[136] X. Wu, J.G. Sun, S. Lu, M.H. Yin. Propositional Extension Rule with Reduction. International Journal of Computer Science and Network Security, 2006, 6: 190-195.
[137] J. Hooker. Solving the incremental satisfiability problem. Journal of Logic Programming, 1993, 15: 177-186.
[138] J. W. Lloyd. Foundations of logic programming. Springer-Verlag, Berlin, 1987.
[139] H. Ganzinger and K. Korovin. New directions in instantiation-based theorem proving. In: Proc. of 8th Annual IEEE Symposium on Logics in Computer Science (LICS 2003), Ottawa, Canada, 2003, 55-64.
[140] C. Chang and R. C. Lee. Symbolic logic and mechanical theorem proving, Academic Press, 1973.
[141] H. Chu and D.A. Plaisted. Semantically guided first-order theorem proving using hyper-linking. In: Proc. of 12th Conference on Automated Deduction, Nancy, France, 1994, 192-206.
[142] M. Paramasivam and A. D. Plaisted. A replacement rule theorem prover. Journal of Automated Reasoning, 1997, 18:221-226.
[143] R. G. Jeroslow. Computation-oriented reductions of predicate to propositional logic. Decision Support Systems, 1988, 4:183-197.
[144] H. Kautz and B. Selman. Planning as satisfiability. In: Proc. of 10th European Conference on Artificial Intelligence (ECAI 1992), Vienna, Austria, 1992, 359-363.
[145] P. Blachburn, M. Rijke and Y. Venema. Modal logic. Cambridge University Press, 2001.
[146] K. Fine. Normal forms in modal logic. J. Notre Dame ed., Formal Logic, 1975, 16: 229-237. R. Lander. The Computational Complexity of Provability in Systems of Modal Logic. SIAM Journal on Computing, 6:467-480.
[147] H. J. Ohlbach, A. Nonnengart, M. de Rijke and D. M. Gabbay. Encoding tow-valued non-classical logics in classical logic. In: Robinson and A. Voronkov, eds., Handbook of Automated Reasoning, Elsevier Science Publishers, 2001, 1403-1487.
[148] D. M. Gabby. An irreflexivity lemma with applications to axiomatizations of conditions on linear frames. In U. M?nnich, ed., Aspects of Philosophical Logic, Reidel, 1981, 67-89.
[149] R. Ladner. The computational complexity of provability in systems of modal logic. SIAM Journal on Computing, 1977, 6: 467-480.
[150] M. Vardi. Why is modal logic so robustly decidable. In DIMACS Series in Discrete Mathematics and Theoretical Computer Science, AMS, 1997, 149-184.
[151].H. Ganzinger and H. De Niverlle. A superposition decision procedure for the guarded fragment with equality. In: Proc. of 14th IEEE Symposium on Logic in Computer Science (LICS 1999), Trento, Italy, 1999, 295-304.
[152] C. Areces, R. Gennari, J. Heguiabehere and M. De rijke. Tree-based heuristics for modal theorem proving. In: Proc. of 14th European Conference on Artificial Intelligence (ECAI 2000), 2000, 199-203.
[153] H. J. Ohlbach. A resolution calculus for modal logics. In Proc. of 9th International Conference on Automated Deduction (CADE 1988), Argonne, IL, USA, 1988, 500-516.
[154] M. C. Fitting. Destructive modal resolution. Journal of Logic and Computation, 1990, 1:83-97.
[155] M. C. Fitting. Proof methods for modal and intuitionistic logics. D. Reidel Publishing Company, Kruwer, 1983.
[156] L. Fari?as del Cerro and A. Herzig. Linear modal deductions. In Proc. of 9th International Conference on Automated Deduction (CADE 1988), Argonne, IL, USA, 1988, 487-499.
[157] A. Herzig. Raisonnement automatique en Logique modale et algorithms d'unification. PhD thesis, Université, Toulouse, 1989.
[158] N. Zamov. Modal resolution. Soviet Math, 1989, 33: 22-29.
[159] Y. Auffray and P. Enjalbert. Modal theorem proving: An equational viewpoint. Journal of Logic and Computation, 1992, 2(3): 247-297.
[160] J. van Benthem. Beyond accessibility: Functional models for modal logic. In M. de Rijke ed., Diamonds and Defaults, Kluwer, 1993.
[161] D. M. Gabby and H. J. Ohlbach. Quantifier elimination in second-order predicate logic. Journal of South African Computer, 1992, 7: 35-43.
[162] H. J. Ohlbach. Semantic based translation methods for modal logics. Journal of Logic and Computation, 1991, 1(5): 691-746.
[163] H. J. Ohlbach, D. M. Gabby and D. Plaisted. Killer transformations. Research Report MPI-I-94_226, Max-Planck-Institut für Infomatik, Saarbrücken, 1997.
[164] A. Herzig. A new decidable fragment of first order logic. In Abstracts of the 3rd Logical Biennal, Summer School and Conference in Honour of S. C. Kleen, Varna, Bulgaria, 1990.
[165] W. C. Purdy. Decidability of fluted logic with identity. Notre Dame Journal of Formal Logic, 1996, 37(1): 84-104.
[166] W. C. Purdy. Fluted formulas and the limits of decidability. Journal of Symbolic Logic, 1996, 61(2): 608-620.
[167] X. Wu., J.G. Sun, H. Lin and S. S. Feng. Modal extension rule. Process In Natural Science, China, 2005, 15(6): 550-558.