若干逻辑自动推理方法研究
|
摘要
自动定理证明(Automated Theorem Proving)或者机器定理证明(MechanicalTheorem Proving)是通过计算机实现定理证明.二十世纪五十年代以来自动定理证明一直是计算机科学的热点之一,在数学、硬件测试与验证、软件生成与验证、协议验证、人工智能方面都得到了成功的应用.
部分实例化方法把一阶问题化为一系列命题逻辑中的可满足性问题来解决一阶逻辑的可满足问题,检查子句集的满足式映射中的阻塞是该方法的关键.论文提出的子句搜索方法在判定子句集可满足性的同时给出了一个模型从而得到满足式映射.格值逻辑的不完全可比性便于描述人类的思维、判断和决策.格值命题逻辑系统LP(X)于1993年建立,目前对LP(X)系统的自动推理研究主要是归结方法,论文讨论了它的tableau方法.常用的逻辑证明方法重点在于判定可满足性而不能给出符合人们阅读习惯的演绎过程.归结方法、语义表方法、相继式方法是定理证明中的常用方法,但是重点在于判定而不是演绎,论文探讨了相干命题逻辑系统R的试探法实现和相干自然推理系统NR的自然推理法实现,生成了类似于手工证明的可读证明.具体而言论文的工作包括以下几方面:
(1)提出了子句搜索方法判定命题子句集的可满足性并给出可满足子句集的一个模型.子句搜索方法通过查找到子句集Φ不可扩展的子句C来判定Φ的可满足性.结合部分实例化方法将子句搜索方法提升至一阶,分离了谓词公式的结构和变量,从而提高合一算法的效率并节省了存贮空间.用正整数代表原子,负整数代表负文字,简化了算法实现.
(2)提出了格值命题逻辑系统LP(X)的tableau方法,语义表中的公式都是受限蕴涵公式.通过引入Bound~s(X)、Bound_s(X)和极大相容集证明了其正确性和完备性.对于真值域可直积分解的系统LP(X),讨论了其格直积分解证明.
(3)提出了后推试探证明方法并将演绎序列中的各公式组织成证明树从而产生了类似于手工证明的演绎序列.将公式转化为二叉树的形式存贮于动态数组中减小了公式冗余,用数组下标代表公式简化了实现.
(4)提出了应用于自然推理方法的回溯方法.先从假设集出发构建证明树,再从树根节点逐层推导各公式的属性,实现了相干自然推理系统NR的类似手工证明的自然推理方法证明.
综上所述,论文提出了判定子句集可满足性的子句搜索方法并将其提升至一阶,提出了格值命题逻辑系统LP(X)的tableau方法,提出了后推试探方法和回溯方法并实现了相干命题逻辑系统R的可读证明,在理论和应用方面都有积极意义.
Automated theorem proving or mechanical theorem proving is concerned with the building of computing systems that automate the process of proving theorems. Since the 1950s ATP has been one of active research topics of computer science and successfully used in mathematics, hard test and verification, software generation and verification, protocol verification, and artificial intelligence.
The partial instantiation method reduces satisfiability problems for first-order logic to a series of ground-level satisfiability problems. Finding out the blockages of satisfier mappings for clause set is necessary in this method. Clause searching method proposed by us not only decides the satisfiability of clause set but also presents a model then obtains a satisfier mapping. Lattice-valued logic is not completely comparable and proper to describing thinking, judging and decision-making. Lattice-valued propositional logic system LP(X) is proposed in 1993. At present automated reasoning research about LP(X) focuses on resolution method, this thesis discusses tableau method for LP(X). The usual deduction methods such as resolution method, tableau method, sequent calculus etc emphasis on decidability instead of deduction. This thesis discusses implementing probing method and natural deduction method for relevant propositional R, and generates readable deduction sequences similar to humans'. The main content is as follows:
(1) Proposing clause searching method which decides satisfiability of clause setΦand presents a model for satisfied set. This method decides satisfiability by searching one clause which can not extended fromΦ. Updating clause searching method to first-order by use of partial instantiation methods. This thesis separates predicate formulae into two parts: structures and variables hence improves unification algorithm efficiency and saves storage space. We establish a mapping of one atom onto one positive integer and one negative word onto one negative integer.
(2) Proposing tableau method for lattice-valued propositional system LP(X), and all formulae is bounding implications. By introducing concepts such as Bound~s(X), Bound_s(X) and maximally consistent set, we prove this method's correctness and completeness. If truth value space L of system LP(X) is the direct product of L_i, then we can prove theorems in LP(X) by means of direct decomposition.
(3) Proposing backward probing method, obtaining a proof tree consisting of formulae in deduction sequences, and generating readable deduction sequences similar to humans'. We reduce formulae redundancy by transforming formulae into binary tree forms and storing them in a dynamic array, then array subscripts stand for formulae.
(4) Proposing backtrace method applied to natural deduction method. Firstly constructing a proof tree from hypothesis set, then starting from tree root we obtain formulae attributes layer by layer. The thesis implements natural deduction method for relevant natural deduction system NR and generates readable deduction sequences similar to humans'.
In conclusion, this thesis proposes clause searching method to check satisfiability of clause set, lifts the new method to first-order, proposes tableau method for latticed-valued logic system LP(X), proposes backward probing method and backtrace method, generates readable proof for relevant propositional logic and has a positive meaning in the theory and application.
部分实例化方法把一阶问题化为一系列命题逻辑中的可满足性问题来解决一阶逻辑的可满足问题,检查子句集的满足式映射中的阻塞是该方法的关键.论文提出的子句搜索方法在判定子句集可满足性的同时给出了一个模型从而得到满足式映射.格值逻辑的不完全可比性便于描述人类的思维、判断和决策.格值命题逻辑系统LP(X)于1993年建立,目前对LP(X)系统的自动推理研究主要是归结方法,论文讨论了它的tableau方法.常用的逻辑证明方法重点在于判定可满足性而不能给出符合人们阅读习惯的演绎过程.归结方法、语义表方法、相继式方法是定理证明中的常用方法,但是重点在于判定而不是演绎,论文探讨了相干命题逻辑系统R的试探法实现和相干自然推理系统NR的自然推理法实现,生成了类似于手工证明的可读证明.具体而言论文的工作包括以下几方面:
(1)提出了子句搜索方法判定命题子句集的可满足性并给出可满足子句集的一个模型.子句搜索方法通过查找到子句集Φ不可扩展的子句C来判定Φ的可满足性.结合部分实例化方法将子句搜索方法提升至一阶,分离了谓词公式的结构和变量,从而提高合一算法的效率并节省了存贮空间.用正整数代表原子,负整数代表负文字,简化了算法实现.
(2)提出了格值命题逻辑系统LP(X)的tableau方法,语义表中的公式都是受限蕴涵公式.通过引入Bound~s(X)、Bound_s(X)和极大相容集证明了其正确性和完备性.对于真值域可直积分解的系统LP(X),讨论了其格直积分解证明.
(3)提出了后推试探证明方法并将演绎序列中的各公式组织成证明树从而产生了类似于手工证明的演绎序列.将公式转化为二叉树的形式存贮于动态数组中减小了公式冗余,用数组下标代表公式简化了实现.
(4)提出了应用于自然推理方法的回溯方法.先从假设集出发构建证明树,再从树根节点逐层推导各公式的属性,实现了相干自然推理系统NR的类似手工证明的自然推理方法证明.
综上所述,论文提出了判定子句集可满足性的子句搜索方法并将其提升至一阶,提出了格值命题逻辑系统LP(X)的tableau方法,提出了后推试探方法和回溯方法并实现了相干命题逻辑系统R的可读证明,在理论和应用方面都有积极意义.
Automated theorem proving or mechanical theorem proving is concerned with the building of computing systems that automate the process of proving theorems. Since the 1950s ATP has been one of active research topics of computer science and successfully used in mathematics, hard test and verification, software generation and verification, protocol verification, and artificial intelligence.
The partial instantiation method reduces satisfiability problems for first-order logic to a series of ground-level satisfiability problems. Finding out the blockages of satisfier mappings for clause set is necessary in this method. Clause searching method proposed by us not only decides the satisfiability of clause set but also presents a model then obtains a satisfier mapping. Lattice-valued logic is not completely comparable and proper to describing thinking, judging and decision-making. Lattice-valued propositional logic system LP(X) is proposed in 1993. At present automated reasoning research about LP(X) focuses on resolution method, this thesis discusses tableau method for LP(X). The usual deduction methods such as resolution method, tableau method, sequent calculus etc emphasis on decidability instead of deduction. This thesis discusses implementing probing method and natural deduction method for relevant propositional R, and generates readable deduction sequences similar to humans'. The main content is as follows:
(1) Proposing clause searching method which decides satisfiability of clause setΦand presents a model for satisfied set. This method decides satisfiability by searching one clause which can not extended fromΦ. Updating clause searching method to first-order by use of partial instantiation methods. This thesis separates predicate formulae into two parts: structures and variables hence improves unification algorithm efficiency and saves storage space. We establish a mapping of one atom onto one positive integer and one negative word onto one negative integer.
(2) Proposing tableau method for lattice-valued propositional system LP(X), and all formulae is bounding implications. By introducing concepts such as Bound~s(X), Bound_s(X) and maximally consistent set, we prove this method's correctness and completeness. If truth value space L of system LP(X) is the direct product of L_i, then we can prove theorems in LP(X) by means of direct decomposition.
(3) Proposing backward probing method, obtaining a proof tree consisting of formulae in deduction sequences, and generating readable deduction sequences similar to humans'. We reduce formulae redundancy by transforming formulae into binary tree forms and storing them in a dynamic array, then array subscripts stand for formulae.
(4) Proposing backtrace method applied to natural deduction method. Firstly constructing a proof tree from hypothesis set, then starting from tree root we obtain formulae attributes layer by layer. The thesis implements natural deduction method for relevant natural deduction system NR and generates readable deduction sequences similar to humans'.
In conclusion, this thesis proposes clause searching method to check satisfiability of clause set, lifts the new method to first-order, proposes tableau method for latticed-valued logic system LP(X), proposes backward probing method and backtrace method, generates readable proof for relevant propositional logic and has a positive meaning in the theory and application.
引文
[1]C.L.Chang and R.C.T.Lee.Symbolic Logic and Mechanical Theorem Proving.Academic Press,New York,1973
[2]D.W.Loveland.Automated Theorem Proving:A Logical Basis.North-Holland,Elsevier,Amsterdam,New York,1978
[3]W.Bibel.Automated Theorem Proving.File&.Vieweg & Sohn,Braunschweig,1987
[4]H.Gelemter.Realization of a geometry theoremproving machine,Proceedings of an International Conference on Information Processing,Pads:UNESCO House,1959.pp.273-282.
[5]D.A.Duffy.Principles of Automated Theorem Proving.John Wiley & Sons Ltd,Chichester,1991
[6]冯棉.逻辑学的历史与现状-兼纪念哥德尔诞辰100周年.科学,58(3):53-56,2006 Harvard University Press.1 967
[7]A.Church.A note on the Entseheidungsproblem.The Journal of Symbolic Logic,1(1):40-41,1936
[8]A.M.Turing.On computable numbers,with an application to the Entscheidungsproblem.Procedings of the London Mathematical Society,42:230-265,1936
[9]W.Ackermann.Solvable Cases of the Decision Problem.North-Holland Pub.Co,Amsterdam,1954
[10]B.Dreben,W.D.Goldfarb.The Decision Problem:Solvable Classes of QuantificationalFormulas.Addison-Wesley,Reading,Massachusetts,1979
[11]E.B(o|¨)rger,E.Gr(a|¨)del,Y.Gurevich.The Classical Decision Problem.Springer,Berlin,1997
[12] A. Newell, J. C. Shaw, H. A. Simon. Empirical explorations with the Logic Theory Machine. In: Proc. of West. Joint Comp. Conf., 218-239, 1957.
113] R. G. Jeroslow. Computation-oriented reductions of predicate to propositional logic.Decision Support Systems, 4: 183-197,1988
[14] P. C. Gilmore. A proof method for quantification theory: Its justification and realization. IBM Journal of Research and Development, 4: 28-35,1960
[15] H. Wang. Toward mechanical mathematics. IBM Journal of Research and Development, 4: 2-22,1960
[16] M. Davis, H. Putnam. A computing procedure for quantification theory. J. ACM,7(3): 201-215,1960
[17] D. Prawitz. An improved proof procedure. In: J. H. Siekmann, G. Wrightson,eds. Automation of Reasoning: Classical Papers on Computational Logic, Vol. 1.Springer, Berlin, 1983. pp. 159-199
[18] J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM,12(1): 23-41, 1965
[19] L. Wos, D. Carson, G. A. Robison. Efficiency and completeness of the set of support strategy in theorem proving, J. ACM, 12(4): 536-541, 1965
[20] R. Anderson, W. W. Bledsoe. A linear format for resolution with merging and a new technique for establishing completeness. In: J. H. Siekmann, G. Wrightson,eds. Automation of Reasoning: Classical Papers on Computational Logic, Vol. 2.Springer, Berlin, 1983. pp. 321-330
[21 ] J.R.Slagle. Automatic Theorem Proving With Renamable and Semantic Resolution.Journal of ACM, 14(4), 1967. pp. 687-697
[22] R.Kowaski, D.Kuehner. Linear Resolution with Selection Function. Artificial Intelligence, Vol.2, 1971
[23] D.W. Loveland. A linear format for resolution. In: J. H. Siekmann, G. Wrightson,eds. Automation of Reasoning: Classical Papers on Computational Logic, Vol. 2.Springer, Berlin, 1983. pp. 542-575
[24]C.L.Chang.The unit proof and the input proof in theorem proving.J.ACM,17(4):698-707,1970
[25]L.Wos,D.Carson,G.A.Robinson.The unit preference stategy in theorem proving.Proc.AFIPS,1964,Fall Joint Comput.Conf.26,pp.616-621
[26]N.V.Murray.Completely Non-linear Theorem Proving.Artificial Intelligence,18(1),1982.pp.67 - 85
[27]J.A.Robinson.Automated deduction with hyper-resolution.International J.Computer Mathematics,1:227-234,1965
[28]陆汝钦.Horn集的消解原理.中国科学(A辑).24(7):896-903,1981
[29]陆汝钦.强有序输入消解原理.中国科学(A辑).24(8):1035-1042,1981
[30]刘叙华.基于归结方法的自动推理.北京:科学出版社,1994
[31]C.L.Chang,R.C.T.Lee.Symbolic Logic and Mechanical Theorem Proving.Academic Press,1973
[32]程晓春,孙吉贵,刘叙华,模态逻辑D演化过程的化简规则.吉林大学自然科学学报.(2):39-43,1995
[33]程晓春,刘叙华.标记逻辑的TABLEAU判定过程.软件学报.7(11):698-705,1996
[34]程晓春.BAOFL的Tableau推理.吉林大学自然科学学报.(1):39-42,1997
[35]程晓春,姜云飞.关于择优蕴涵的悖论.计算机研究与发展.34(2):81-86,1997
[36]刘叙华,司徒芊.广义λ-调解.计算机学报.18(2):135-140,1995
[37]刘瑞胜,孙吉贵,刘叙华.带有约束的缺省逻辑.吉林大学自然科学学报.(3):1-4,1996
[38]孙吉贵,刘叙华.强模态归结.吉林大学自然科学学报.(1):25-29,1996
[39]孙吉贵,刘叙华.模态归结弱包含删除策略.计算机学报.17(5):321-330,1994
[40]孙吉贵,李乔,刘叙华.模态K_4、D_4系统的归结推理.软件学报.6(12):742-750,1995
[41]王元元.广义替换归结方法.南京大学学报.(2):205-209,1986
[42]王元元.计算机科学中的现代逻辑学.北京:科学出版社,2001
[43]陆汝占,林凯,孙永强.着色归结、PI着色碰撞及其完备性.计算机学报.(12):720-727.1987
[44]G.D.Alexander.CLIN-E-Smallest instance first hyper-linking.Journal of Automated Reasoning.18(2):177-182,1997
[45]H.Chu,D.A.Plaisted.CLIN-S-A semantically guided first-order theorem prover.Journal of Automated Reasoning.18(2):183-188,1997
[46]C.B.Suttner,G.Sutcliffe.The design of the CADE-13 ATP system competition.Journal of Automated Reasoning.18(2):139-162,1997
[47]G.A.Robinson,L.Wos.Paramodulation and theorem proving in first order theories with equality.In:B.Meltzer,D.Michie eds.Machine Intelligence,Vol.4,American Elsevier,New York,1969.pp.135-150
[48]W.W.Bledsoe.Non-Resolution Theorem Proving.Artificial Intelligence,Vol.9,1977.pp.1-35
[49]D.E.Knuth,P.B.Bendix.Simple word problems in universal algebras.In:J.Leech,ed.Computational Problems in Abstract Algebra.Pergamom,New York,1970.pp.263-267
[50]D.Beauquier,A.Slissenko.A first order logic for specification of timed algorithms:basic properties and a decidable class.Annals of Pure and Applied Logic,113:13-53,2002
[51]I.Hodkinson,F.Wolter,M.Zakharyaschev.Decidable fragments of first-order temporal logics.Annals of Pure and Applied Logic,106:85-134,2000
[52]D.Beauquier,A.Slissenko.Decidable verification for reducible timed automata specified in first order logic with time.Theoretical Computer Science,275:347-388,2002
[53]T.J.Weigert,J.J.-P.Tsai.A computationally tractable nonmonotonic logic.IEEE Trans.Knowledge and Data Enigeering,6(1):57-63,1994
[54] A. del Val. On some tractable classes in deduction and abduction. Artificial Intelligence, 116: 297-313,2000
[55] D. Mcallester, R. Givan. Taxonomic syntax for first order inference. J. ACM, 40(2):246-283,1993
[56] N. Friedman, J. Y. Halpern, D. Koller. First-order conditional logic for default reasoning revisited. ACM Trans. Computational Logic, 1(2): 175-207,2000
[57] P. Liberatore. Monotonic reductions, representative equivalence, and compilation of intractable problems. J. ACM, 48(6): 1091-1125,2001
[58] H. Kautz, M. Kearns, B. Selman. Horn approximations of empirical data. Artificial Intelligence, 74: 129-145,1995
[59] R. Khardon, D. Roth. Reasoning with models. Artificial Intelligence, 87: 187-213,1996
[60] B. Selman, H. Kautz. Knowledge compilation and theory approximation. J. ACM,43(2): 193-224,1996
[61] P. Liberatore. Compilability and compact representations of revision of Horn Knowledge bases. ACM Trans. Computational Logic, 1(1): 131-161,2000
[62] T. Eiter, T. Ibaraki, K. Makino. Computing intersections of Horn theories for reasoning with models. Artificial Intelligence, 110: 57-101,1999
[63] T. Horiyama, T. Ibaraki. Ordered binary decision diagrams as knowledge-bases. Artificial Intelligence, 136: 189-213,2002
[64] R. Khardon, D. Roth. Leaning to reason. J. ACM, 44(5): 697-725,1997
[65] R. Geriner, C. Darken, N. Iwan Santoso. Efficient reasoning. ACM Computing Surveys, 33(1): 1-30,2001
[66] G. Lakemeyer. Limited reasoning in first-order knowledge bases with full introspection. Artificial Intelligence, 84: 209-255,1996
[67] A. Y. Levy, R. E. Fikes, Y. Sagiv. Speeding up inferences using relevance reasoning:a formalism and algorithms. Artificial Intelligence, 97: 83-136,1997
[68]C.Vilhelm,P.Ravaux,D.Calvelo,et al.Think!:a unified numerical-symbolic knowledge representation schema and reasoning systems.Artificial Intelligence,116:67-85,2000
[69]吴文俊.初等几何判定问题与机械化证明.中国科学,(6):507-516,1977
[70]吴文俊.几何定理机器证明的基本原理.北京:科学出版社,1984
[71]高小山.数学机械化进展综述.数学进展,30(5):385-404,2001
[72]高小山,张景中,周咸青.几何专家.台北:九章出版社,1998
[73]自动推理平台,http://www.mmrc.iss.ac.cn/gex
[74]张景中.几何定理机器证明二十年.科学通报,42(21):2248-2259,1997
[75]张景中,杨路,高小山,等.几何定理可读证明的自动生成.计算机学报,18(5):380-393,1995
[76]张景中.面积关系帮你解题.上海:上海教育出版社,1982
[77]杨路,张景中,侯晓荣.非线性方程组与定理机器证明.上海:上海科技教育出版社,1996
[178]杨路,夏时洪.一类构造性集合不等式的机器证明.计算机学报,26(7):769-778,2003
[79]杨路.计算机怎样证明几何不等式.广州大学学报(自然科学版),(02),2004
[80]杨路,侯晓荣,夏壁灿.自动发现不等式型定理的一个完备算法.中国科学E辑,(3),2001
[81]曾振柄,陈良育,张骏,符红光.基于AJAX和自动推理技术构建交互式数学Web服务.计算机应用,27(9):2239-2241,2007
[82]符红光,赵世忠.构造一般Dixon结式矩阵的快速算法.中国科学A辑,35(1):1-14.2005
[83]符红光,杨路,曾振柄.构造广义Sturm序列的递归算法.中国科学E辑,29(6):546-555,1999
[84]姚勇,冯勇.一类半正定多项式的平方和分解及其表达式的自动生成.计算机学报,29(10):1862-1868,2006
[85]杨路,姚勇,冯勇.Tarski模型外的一类机器可判定问题.中国科学A辑,37(5):513-522,2007
[86]张景中,冯勇.采用近似计算获得准确值.中国科学A辑,37(7):809-816,2007
[87]J.Denzinger,M.Kronenburg,S.Schulz.DISCOUNT-a distributed and learning equational prover.Journal of Automated Reasoning.18(2):189-198,1997
[88]W.McCune,L.Wos.Otter:The CADE-13 competition incarnations.Journal of Automated Reasoning.18(2):211-220,1997
[89]R.Nieuwenhuis,J.M.V.Rivero,M.A.Vallejo.Barcelona.Journal of Automated Reasoning.18(2):171-176,1997
[90]J.Lukasiewicz.On 3-valued logic.Ruch Filozoficizny,5:169-170,1920
[91]E.Post.Introduction to a general theory of elemnetary propositions.American Journal of Mathematics,43:163-185,1921
[92]D.A.Bochver.On 3-valued logic calculus and its application to the analysis of contraditions.Mathematiceskij Sbornik,4:287-308,1939
[93]S.C.Kleene.Introduction to Metamathematics.New York:Van Nostrand,1952
[94]L.A.Zadeh.Fuzzy Sets.Inf.Control,8:338-353,1965
[95]J.A.Goguen.The logic of inexact concepts.Synthese,19:325-373,1969
[96]J.Pavalka.On fuzzy logic Ⅰ:Many-valued rules of inference.Zeitschr.f.Math.Logik und Grundlagend.Math.,25:45-52,1979
[97]J.Pavalka.On fuzzy logic Ⅱ:Enriched residuated lattice and semantics of propositional calculi.Zeitschr.f.Math.Logik und Grundlagend.Math.,25:119-134,1979
[98]J.Pavalka.On fuzzy logic Ⅲ:Semantical completeness of some many-valued propositional calculi.Zeitschr.f.Math.Logik und Grundlagend.Math.,25:447-464,1979
[99]X.H.Liu,H.Xiao.Operator fuzzy logic and fuzzy resolution.Proceeding of the 5th IEEE International Symp on Multi-valued Iogic(ISMUL 85),1985
[100]朱梧桢,肖奚安.中介逻辑的命题演算系统(Ⅰ),(Ⅱ),(Ⅲ).自然杂志.8:315,394,473,1985
[101]朱梧槚,肖奚安.中介逻辑的命题演算的扩张(Ⅰ),(Ⅱ).自然杂志.8:681,716,1985
[102]王国俊.非经典数理逻辑与近似推理.北京:科学出版社,2000
[103]王国俊.模糊推理的全蕴涵三I算法.中国科学(E辑),19(1):43-53,1999
[104]王国俊.三I方法与区间值模糊推理.中国科学(E辑),30(4):331-340,2000
[105]冯棉.广义模态逻辑.上海:上海华东师范大学出版社,1990
[106]冯棉.经典逻辑与直觉主义逻辑.上海:上海人民出版社,1989
[107]冯棉.相干与衍推逻辑.上海:上海人民出版社,1993
[108]冯棉.论相干逻辑的研究方法.华东师范大学学报(哲学社会科学版),40(6):58-62,2008
[109]周昌乐.认知逻辑导论.清华大学出版社,2001
[110]李未.一种求解合取范式可满足性问题的数学物理方法.中国科学A辑,24(11):1208-1217,1994
[111]刘涛,李国杰.求解SAT问题的分级重排搜索算法.软件学报,7(4):201-210,1996
[112]刘涛,李国杰.求解SAT问题的局部搜索算法及其平均时间复杂性分析.计算机学报,20(1):18-26,1997
[113]黄文奇,金人超.求解SAT问题的拟物拟人算法.中国科学E辑,27(2):179-186.1997
[114]张德富,黄文奇,汪厚祥.求解SAT问题的拟人退火算法.计算机学报,25(2):148-152,2002
[115]李阳阳,焦李成.求解SAT问题的量子免疫克隆算法.计算机学报,30(2):176-183,2007
[116]R.M.Smullyan.First-order logic.Springer,New York,1994
[117]M.Fitting.First-order logic and automated theorem proving.Springer,New York,1996
[118]M.Fitting.Types and Tableau.Berlin:Springer Verlag,2000
[119]R.Hahnle,F.Manya.Transformations between signed and classical clause logic.In:Proc.of ISMVL99,IEEE Press,248-255,1999
[120]W.Bibel.Automated theorem proving.Second edition,Vieweg Vedag,Brauschweig,1987
[121]R.Hahnle.Short conjunctive normal forms in finitely-valued logics.Journal of Logic and Computatiion,4(6):905-927,1994
[122]F.M.Brown.Towards the automation of set theory and its logic.Artificial Intelligence,10(3):281-316,1978
[123]K.S.Brace,R.L.Rudell,R.E.Bryant.Efficient implementation of a BDD package.In:Proc.27th ACM/IEEE Design Automation Conference,Los Alamitos,40-45,1990
[124]徐扬.格蕴涵代数.西南交通大学学报.1993,1:20-27
[125]徐扬.格蕴涵代数中的同态.中国第五届多值逻辑学术会议论文集,南京.1992,206-210
[126]徐扬,秦克云.格蕴涵代数的格论性质.应用数学文集,成都:成都科技大学出版社,54-58,1992
[127]徐扬,秦克云.格蕴涵代数中的(S)条件.运筹与决策,成都:成都科技大学出版社,2039-2044,1992
[128]刘军,徐扬.格蕴涵代数中性质(P)的讨论.兰州大学学报(自然科学版),32:344-348,1996
[129]徐扬.格蕴涵代数与BCK代数的关系.模糊系统与数学,11(1):10-15,1997
[130]宋振明,徐扬.格蕴涵代数上的同余关系.应用数学,10(3):121-124,1997
[131]刘军,徐扬.格值命题逻辑系统LP(X)的语法问题.西南交通大学百周年校庆论文集,成都:西南交通大学出版社,305-308:1996
[132]秦克云,徐扬.格值命题逻辑系统L(X)(Ⅰ).模糊系统与数学,11(4):5-11,1997
[133]秦克云,徐扬.格值命题逻辑系统L(X)(Ⅱ).模糊系统与数学,12(1):10-19,1998
[134]徐扬,邹开其.布尔逻辑公式中文字和小项的可消性.西南交通大学学报,75(1):107-112,1990
[135]徐扬,宋振明.格值逻辑公式中短语和文字的可消性.数学季刊,5(1,2):172-180.1990
[136]土伟,徐扬,秦克云.格值命题逻辑LP(X)中不可分极简式的性质.模糊系统与数学,18(1),2004
[137]Y.Xu,K.Y.Qin.Lattice-valued propositional logic(I).Journal of Southwest Jiaotong University,2:123-128,1993
[138]K.Y.Qin,Y.Xu.Lattice-valued propositional logic(II).Journal of Southwest Jiaotong University,2:22-27,1994
[139]Y.Xu,K.Y.Qin,E.H.Ron.A First Order Lattice Valued Logic System Ⅰ:Semantics.The Journal of Fuzzy Mathematics,4(9):969-976,2001
[140]K.Y.Qin,Y.Xu.E.H.Ron.A First Order Lattice Valued Logic System Ⅱ:Syntax.The Journal of Fuzzy Mathematics,4(9):977-983,2001
[141]Y.Xu,K.Y.Qin,J.Liu,Z.M.Song.L-valued propositional logic L_(vpl),Int.J.Information Sciences,114:205-235,1999
[142]Y.Xu,J.Liu,Z.M.Song,K.Y.Qin.On semantics of L-valued first-order logic L_(vfl).Int.J.General Systems,Vol.29(1):53-79,2000
[143]Y.Xu,Z.M.Song,K.Y.Qin,J.Liu.Syntax of L-valued forst-order Logic L_(vfl).Int.Multi.Val.Logic,7:213-257,2001
[144]Y.Xu,D.Ruan,K.Y.Qin,L.Jun.Lattice-valued logic.Springer-Verlag Berlin Heidelberg,2003
[145]Y.Xu,D.Ruan,E.E.Kerre et al.α-Resolution principle based on lattice-valued logic LP(X).information Science 130,195-223,2000
[146]Y.Xu,D.Ruan,E.E.Kerre et al.α-Resolution principle based on first-order lattice-valued LF(X),Information Science,132,221-239,2001
[147] W. Wang, Y. Xu, X. F. Wang. α-automated reasoning method based on lattice-valued propositional logic LP(X), Journal of Southwest Jiaotong University,10(1):98-111,2002
[148] A. Urquhart. The undecidability of entailment and relevant implication. The Journal of Symbolic Logic, 49(4): 1059-1073,1984
[149] K. Fine. Semantics for quantified relevance logic. Journal of Philosophical Logic,17(1), 1988
[150] X. Wu, J. G. Sun, K. Hou. Extension rule in first order logic. In: Proc. of 5th International Conference on Cognitive Informatics (ICCI 2006), Beijing, China, 2006,pp.701-706
[151] H. Lin, J. G. Sun, Y. M. Zhang. Theorem proving based on extension rule. Journal of Automated Reasoning, Springer, Berlin, 31: 11-21,2003
[152] X.Wu, J.G.Sun, K.Hou. An extension rule based first-order theorem proven In:Proc. of 1st International Conference on Knowledge Science, Engineering and Management(KSEM 2006), Guilin, China, 2006, pp.514-524
[153] X.Wu, J.G.Sun, S.Lu et al. Improved propositional extension rule. In:Proc. of 1st International Conference on Rough Sets and Knowledge Technology(RSKT2006),Chongqing, China, 2006, pp.592-597
[154] J. N. Hooker, G. Rago, V. Chandru, A. Shrivastava. Partial instantiation methods for inference in first-order Logic. Journal of Automated Reasoning, 28: 371-396,2002
[155] H. Ganzinger, 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, 55-64, 2003
[156] L. Wos et al. Automated Reasoning: Introduction and Applications. McGraw-Hill,New York, 1992
[157] C. Walther. A mechanical solution of Schubert's Streamroller by many-sorted resolution. Aritificial Intelligence, 26(2): 217-224, 1986
[158] A. G. Hamilton. Logic for Mathematicians. Tsinghua University Press, 2003
[159] R. Zabel. Proof theory of finite-valued logics. [PH D dissertation]. Institut for Algebra and Diskrete Mathematic, TU Wien, 1993
[2]D.W.Loveland.Automated Theorem Proving:A Logical Basis.North-Holland,Elsevier,Amsterdam,New York,1978
[3]W.Bibel.Automated Theorem Proving.File&.Vieweg & Sohn,Braunschweig,1987
[4]H.Gelemter.Realization of a geometry theoremproving machine,Proceedings of an International Conference on Information Processing,Pads:UNESCO House,1959.pp.273-282.
[5]D.A.Duffy.Principles of Automated Theorem Proving.John Wiley & Sons Ltd,Chichester,1991
[6]冯棉.逻辑学的历史与现状-兼纪念哥德尔诞辰100周年.科学,58(3):53-56,2006 Harvard University Press.1 967
[7]A.Church.A note on the Entseheidungsproblem.The Journal of Symbolic Logic,1(1):40-41,1936
[8]A.M.Turing.On computable numbers,with an application to the Entscheidungsproblem.Procedings of the London Mathematical Society,42:230-265,1936
[9]W.Ackermann.Solvable Cases of the Decision Problem.North-Holland Pub.Co,Amsterdam,1954
[10]B.Dreben,W.D.Goldfarb.The Decision Problem:Solvable Classes of QuantificationalFormulas.Addison-Wesley,Reading,Massachusetts,1979
[11]E.B(o|¨)rger,E.Gr(a|¨)del,Y.Gurevich.The Classical Decision Problem.Springer,Berlin,1997
[12] A. Newell, J. C. Shaw, H. A. Simon. Empirical explorations with the Logic Theory Machine. In: Proc. of West. Joint Comp. Conf., 218-239, 1957.
113] R. G. Jeroslow. Computation-oriented reductions of predicate to propositional logic.Decision Support Systems, 4: 183-197,1988
[14] P. C. Gilmore. A proof method for quantification theory: Its justification and realization. IBM Journal of Research and Development, 4: 28-35,1960
[15] H. Wang. Toward mechanical mathematics. IBM Journal of Research and Development, 4: 2-22,1960
[16] M. Davis, H. Putnam. A computing procedure for quantification theory. J. ACM,7(3): 201-215,1960
[17] D. Prawitz. An improved proof procedure. In: J. H. Siekmann, G. Wrightson,eds. Automation of Reasoning: Classical Papers on Computational Logic, Vol. 1.Springer, Berlin, 1983. pp. 159-199
[18] J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM,12(1): 23-41, 1965
[19] L. Wos, D. Carson, G. A. Robison. Efficiency and completeness of the set of support strategy in theorem proving, J. ACM, 12(4): 536-541, 1965
[20] R. Anderson, W. W. Bledsoe. A linear format for resolution with merging and a new technique for establishing completeness. In: J. H. Siekmann, G. Wrightson,eds. Automation of Reasoning: Classical Papers on Computational Logic, Vol. 2.Springer, Berlin, 1983. pp. 321-330
[21 ] J.R.Slagle. Automatic Theorem Proving With Renamable and Semantic Resolution.Journal of ACM, 14(4), 1967. pp. 687-697
[22] R.Kowaski, D.Kuehner. Linear Resolution with Selection Function. Artificial Intelligence, Vol.2, 1971
[23] D.W. Loveland. A linear format for resolution. In: J. H. Siekmann, G. Wrightson,eds. Automation of Reasoning: Classical Papers on Computational Logic, Vol. 2.Springer, Berlin, 1983. pp. 542-575
[24]C.L.Chang.The unit proof and the input proof in theorem proving.J.ACM,17(4):698-707,1970
[25]L.Wos,D.Carson,G.A.Robinson.The unit preference stategy in theorem proving.Proc.AFIPS,1964,Fall Joint Comput.Conf.26,pp.616-621
[26]N.V.Murray.Completely Non-linear Theorem Proving.Artificial Intelligence,18(1),1982.pp.67 - 85
[27]J.A.Robinson.Automated deduction with hyper-resolution.International J.Computer Mathematics,1:227-234,1965
[28]陆汝钦.Horn集的消解原理.中国科学(A辑).24(7):896-903,1981
[29]陆汝钦.强有序输入消解原理.中国科学(A辑).24(8):1035-1042,1981
[30]刘叙华.基于归结方法的自动推理.北京:科学出版社,1994
[31]C.L.Chang,R.C.T.Lee.Symbolic Logic and Mechanical Theorem Proving.Academic Press,1973
[32]程晓春,孙吉贵,刘叙华,模态逻辑D演化过程的化简规则.吉林大学自然科学学报.(2):39-43,1995
[33]程晓春,刘叙华.标记逻辑的TABLEAU判定过程.软件学报.7(11):698-705,1996
[34]程晓春.BAOFL的Tableau推理.吉林大学自然科学学报.(1):39-42,1997
[35]程晓春,姜云飞.关于择优蕴涵的悖论.计算机研究与发展.34(2):81-86,1997
[36]刘叙华,司徒芊.广义λ-调解.计算机学报.18(2):135-140,1995
[37]刘瑞胜,孙吉贵,刘叙华.带有约束的缺省逻辑.吉林大学自然科学学报.(3):1-4,1996
[38]孙吉贵,刘叙华.强模态归结.吉林大学自然科学学报.(1):25-29,1996
[39]孙吉贵,刘叙华.模态归结弱包含删除策略.计算机学报.17(5):321-330,1994
[40]孙吉贵,李乔,刘叙华.模态K_4、D_4系统的归结推理.软件学报.6(12):742-750,1995
[41]王元元.广义替换归结方法.南京大学学报.(2):205-209,1986
[42]王元元.计算机科学中的现代逻辑学.北京:科学出版社,2001
[43]陆汝占,林凯,孙永强.着色归结、PI着色碰撞及其完备性.计算机学报.(12):720-727.1987
[44]G.D.Alexander.CLIN-E-Smallest instance first hyper-linking.Journal of Automated Reasoning.18(2):177-182,1997
[45]H.Chu,D.A.Plaisted.CLIN-S-A semantically guided first-order theorem prover.Journal of Automated Reasoning.18(2):183-188,1997
[46]C.B.Suttner,G.Sutcliffe.The design of the CADE-13 ATP system competition.Journal of Automated Reasoning.18(2):139-162,1997
[47]G.A.Robinson,L.Wos.Paramodulation and theorem proving in first order theories with equality.In:B.Meltzer,D.Michie eds.Machine Intelligence,Vol.4,American Elsevier,New York,1969.pp.135-150
[48]W.W.Bledsoe.Non-Resolution Theorem Proving.Artificial Intelligence,Vol.9,1977.pp.1-35
[49]D.E.Knuth,P.B.Bendix.Simple word problems in universal algebras.In:J.Leech,ed.Computational Problems in Abstract Algebra.Pergamom,New York,1970.pp.263-267
[50]D.Beauquier,A.Slissenko.A first order logic for specification of timed algorithms:basic properties and a decidable class.Annals of Pure and Applied Logic,113:13-53,2002
[51]I.Hodkinson,F.Wolter,M.Zakharyaschev.Decidable fragments of first-order temporal logics.Annals of Pure and Applied Logic,106:85-134,2000
[52]D.Beauquier,A.Slissenko.Decidable verification for reducible timed automata specified in first order logic with time.Theoretical Computer Science,275:347-388,2002
[53]T.J.Weigert,J.J.-P.Tsai.A computationally tractable nonmonotonic logic.IEEE Trans.Knowledge and Data Enigeering,6(1):57-63,1994
[54] A. del Val. On some tractable classes in deduction and abduction. Artificial Intelligence, 116: 297-313,2000
[55] D. Mcallester, R. Givan. Taxonomic syntax for first order inference. J. ACM, 40(2):246-283,1993
[56] N. Friedman, J. Y. Halpern, D. Koller. First-order conditional logic for default reasoning revisited. ACM Trans. Computational Logic, 1(2): 175-207,2000
[57] P. Liberatore. Monotonic reductions, representative equivalence, and compilation of intractable problems. J. ACM, 48(6): 1091-1125,2001
[58] H. Kautz, M. Kearns, B. Selman. Horn approximations of empirical data. Artificial Intelligence, 74: 129-145,1995
[59] R. Khardon, D. Roth. Reasoning with models. Artificial Intelligence, 87: 187-213,1996
[60] B. Selman, H. Kautz. Knowledge compilation and theory approximation. J. ACM,43(2): 193-224,1996
[61] P. Liberatore. Compilability and compact representations of revision of Horn Knowledge bases. ACM Trans. Computational Logic, 1(1): 131-161,2000
[62] T. Eiter, T. Ibaraki, K. Makino. Computing intersections of Horn theories for reasoning with models. Artificial Intelligence, 110: 57-101,1999
[63] T. Horiyama, T. Ibaraki. Ordered binary decision diagrams as knowledge-bases. Artificial Intelligence, 136: 189-213,2002
[64] R. Khardon, D. Roth. Leaning to reason. J. ACM, 44(5): 697-725,1997
[65] R. Geriner, C. Darken, N. Iwan Santoso. Efficient reasoning. ACM Computing Surveys, 33(1): 1-30,2001
[66] G. Lakemeyer. Limited reasoning in first-order knowledge bases with full introspection. Artificial Intelligence, 84: 209-255,1996
[67] A. Y. Levy, R. E. Fikes, Y. Sagiv. Speeding up inferences using relevance reasoning:a formalism and algorithms. Artificial Intelligence, 97: 83-136,1997
[68]C.Vilhelm,P.Ravaux,D.Calvelo,et al.Think!:a unified numerical-symbolic knowledge representation schema and reasoning systems.Artificial Intelligence,116:67-85,2000
[69]吴文俊.初等几何判定问题与机械化证明.中国科学,(6):507-516,1977
[70]吴文俊.几何定理机器证明的基本原理.北京:科学出版社,1984
[71]高小山.数学机械化进展综述.数学进展,30(5):385-404,2001
[72]高小山,张景中,周咸青.几何专家.台北:九章出版社,1998
[73]自动推理平台,http://www.mmrc.iss.ac.cn/gex
[74]张景中.几何定理机器证明二十年.科学通报,42(21):2248-2259,1997
[75]张景中,杨路,高小山,等.几何定理可读证明的自动生成.计算机学报,18(5):380-393,1995
[76]张景中.面积关系帮你解题.上海:上海教育出版社,1982
[77]杨路,张景中,侯晓荣.非线性方程组与定理机器证明.上海:上海科技教育出版社,1996
[178]杨路,夏时洪.一类构造性集合不等式的机器证明.计算机学报,26(7):769-778,2003
[79]杨路.计算机怎样证明几何不等式.广州大学学报(自然科学版),(02),2004
[80]杨路,侯晓荣,夏壁灿.自动发现不等式型定理的一个完备算法.中国科学E辑,(3),2001
[81]曾振柄,陈良育,张骏,符红光.基于AJAX和自动推理技术构建交互式数学Web服务.计算机应用,27(9):2239-2241,2007
[82]符红光,赵世忠.构造一般Dixon结式矩阵的快速算法.中国科学A辑,35(1):1-14.2005
[83]符红光,杨路,曾振柄.构造广义Sturm序列的递归算法.中国科学E辑,29(6):546-555,1999
[84]姚勇,冯勇.一类半正定多项式的平方和分解及其表达式的自动生成.计算机学报,29(10):1862-1868,2006
[85]杨路,姚勇,冯勇.Tarski模型外的一类机器可判定问题.中国科学A辑,37(5):513-522,2007
[86]张景中,冯勇.采用近似计算获得准确值.中国科学A辑,37(7):809-816,2007
[87]J.Denzinger,M.Kronenburg,S.Schulz.DISCOUNT-a distributed and learning equational prover.Journal of Automated Reasoning.18(2):189-198,1997
[88]W.McCune,L.Wos.Otter:The CADE-13 competition incarnations.Journal of Automated Reasoning.18(2):211-220,1997
[89]R.Nieuwenhuis,J.M.V.Rivero,M.A.Vallejo.Barcelona.Journal of Automated Reasoning.18(2):171-176,1997
[90]J.Lukasiewicz.On 3-valued logic.Ruch Filozoficizny,5:169-170,1920
[91]E.Post.Introduction to a general theory of elemnetary propositions.American Journal of Mathematics,43:163-185,1921
[92]D.A.Bochver.On 3-valued logic calculus and its application to the analysis of contraditions.Mathematiceskij Sbornik,4:287-308,1939
[93]S.C.Kleene.Introduction to Metamathematics.New York:Van Nostrand,1952
[94]L.A.Zadeh.Fuzzy Sets.Inf.Control,8:338-353,1965
[95]J.A.Goguen.The logic of inexact concepts.Synthese,19:325-373,1969
[96]J.Pavalka.On fuzzy logic Ⅰ:Many-valued rules of inference.Zeitschr.f.Math.Logik und Grundlagend.Math.,25:45-52,1979
[97]J.Pavalka.On fuzzy logic Ⅱ:Enriched residuated lattice and semantics of propositional calculi.Zeitschr.f.Math.Logik und Grundlagend.Math.,25:119-134,1979
[98]J.Pavalka.On fuzzy logic Ⅲ:Semantical completeness of some many-valued propositional calculi.Zeitschr.f.Math.Logik und Grundlagend.Math.,25:447-464,1979
[99]X.H.Liu,H.Xiao.Operator fuzzy logic and fuzzy resolution.Proceeding of the 5th IEEE International Symp on Multi-valued Iogic(ISMUL 85),1985
[100]朱梧桢,肖奚安.中介逻辑的命题演算系统(Ⅰ),(Ⅱ),(Ⅲ).自然杂志.8:315,394,473,1985
[101]朱梧槚,肖奚安.中介逻辑的命题演算的扩张(Ⅰ),(Ⅱ).自然杂志.8:681,716,1985
[102]王国俊.非经典数理逻辑与近似推理.北京:科学出版社,2000
[103]王国俊.模糊推理的全蕴涵三I算法.中国科学(E辑),19(1):43-53,1999
[104]王国俊.三I方法与区间值模糊推理.中国科学(E辑),30(4):331-340,2000
[105]冯棉.广义模态逻辑.上海:上海华东师范大学出版社,1990
[106]冯棉.经典逻辑与直觉主义逻辑.上海:上海人民出版社,1989
[107]冯棉.相干与衍推逻辑.上海:上海人民出版社,1993
[108]冯棉.论相干逻辑的研究方法.华东师范大学学报(哲学社会科学版),40(6):58-62,2008
[109]周昌乐.认知逻辑导论.清华大学出版社,2001
[110]李未.一种求解合取范式可满足性问题的数学物理方法.中国科学A辑,24(11):1208-1217,1994
[111]刘涛,李国杰.求解SAT问题的分级重排搜索算法.软件学报,7(4):201-210,1996
[112]刘涛,李国杰.求解SAT问题的局部搜索算法及其平均时间复杂性分析.计算机学报,20(1):18-26,1997
[113]黄文奇,金人超.求解SAT问题的拟物拟人算法.中国科学E辑,27(2):179-186.1997
[114]张德富,黄文奇,汪厚祥.求解SAT问题的拟人退火算法.计算机学报,25(2):148-152,2002
[115]李阳阳,焦李成.求解SAT问题的量子免疫克隆算法.计算机学报,30(2):176-183,2007
[116]R.M.Smullyan.First-order logic.Springer,New York,1994
[117]M.Fitting.First-order logic and automated theorem proving.Springer,New York,1996
[118]M.Fitting.Types and Tableau.Berlin:Springer Verlag,2000
[119]R.Hahnle,F.Manya.Transformations between signed and classical clause logic.In:Proc.of ISMVL99,IEEE Press,248-255,1999
[120]W.Bibel.Automated theorem proving.Second edition,Vieweg Vedag,Brauschweig,1987
[121]R.Hahnle.Short conjunctive normal forms in finitely-valued logics.Journal of Logic and Computatiion,4(6):905-927,1994
[122]F.M.Brown.Towards the automation of set theory and its logic.Artificial Intelligence,10(3):281-316,1978
[123]K.S.Brace,R.L.Rudell,R.E.Bryant.Efficient implementation of a BDD package.In:Proc.27th ACM/IEEE Design Automation Conference,Los Alamitos,40-45,1990
[124]徐扬.格蕴涵代数.西南交通大学学报.1993,1:20-27
[125]徐扬.格蕴涵代数中的同态.中国第五届多值逻辑学术会议论文集,南京.1992,206-210
[126]徐扬,秦克云.格蕴涵代数的格论性质.应用数学文集,成都:成都科技大学出版社,54-58,1992
[127]徐扬,秦克云.格蕴涵代数中的(S)条件.运筹与决策,成都:成都科技大学出版社,2039-2044,1992
[128]刘军,徐扬.格蕴涵代数中性质(P)的讨论.兰州大学学报(自然科学版),32:344-348,1996
[129]徐扬.格蕴涵代数与BCK代数的关系.模糊系统与数学,11(1):10-15,1997
[130]宋振明,徐扬.格蕴涵代数上的同余关系.应用数学,10(3):121-124,1997
[131]刘军,徐扬.格值命题逻辑系统LP(X)的语法问题.西南交通大学百周年校庆论文集,成都:西南交通大学出版社,305-308:1996
[132]秦克云,徐扬.格值命题逻辑系统L(X)(Ⅰ).模糊系统与数学,11(4):5-11,1997
[133]秦克云,徐扬.格值命题逻辑系统L(X)(Ⅱ).模糊系统与数学,12(1):10-19,1998
[134]徐扬,邹开其.布尔逻辑公式中文字和小项的可消性.西南交通大学学报,75(1):107-112,1990
[135]徐扬,宋振明.格值逻辑公式中短语和文字的可消性.数学季刊,5(1,2):172-180.1990
[136]土伟,徐扬,秦克云.格值命题逻辑LP(X)中不可分极简式的性质.模糊系统与数学,18(1),2004
[137]Y.Xu,K.Y.Qin.Lattice-valued propositional logic(I).Journal of Southwest Jiaotong University,2:123-128,1993
[138]K.Y.Qin,Y.Xu.Lattice-valued propositional logic(II).Journal of Southwest Jiaotong University,2:22-27,1994
[139]Y.Xu,K.Y.Qin,E.H.Ron.A First Order Lattice Valued Logic System Ⅰ:Semantics.The Journal of Fuzzy Mathematics,4(9):969-976,2001
[140]K.Y.Qin,Y.Xu.E.H.Ron.A First Order Lattice Valued Logic System Ⅱ:Syntax.The Journal of Fuzzy Mathematics,4(9):977-983,2001
[141]Y.Xu,K.Y.Qin,J.Liu,Z.M.Song.L-valued propositional logic L_(vpl),Int.J.Information Sciences,114:205-235,1999
[142]Y.Xu,J.Liu,Z.M.Song,K.Y.Qin.On semantics of L-valued first-order logic L_(vfl).Int.J.General Systems,Vol.29(1):53-79,2000
[143]Y.Xu,Z.M.Song,K.Y.Qin,J.Liu.Syntax of L-valued forst-order Logic L_(vfl).Int.Multi.Val.Logic,7:213-257,2001
[144]Y.Xu,D.Ruan,K.Y.Qin,L.Jun.Lattice-valued logic.Springer-Verlag Berlin Heidelberg,2003
[145]Y.Xu,D.Ruan,E.E.Kerre et al.α-Resolution principle based on lattice-valued logic LP(X).information Science 130,195-223,2000
[146]Y.Xu,D.Ruan,E.E.Kerre et al.α-Resolution principle based on first-order lattice-valued LF(X),Information Science,132,221-239,2001
[147] W. Wang, Y. Xu, X. F. Wang. α-automated reasoning method based on lattice-valued propositional logic LP(X), Journal of Southwest Jiaotong University,10(1):98-111,2002
[148] A. Urquhart. The undecidability of entailment and relevant implication. The Journal of Symbolic Logic, 49(4): 1059-1073,1984
[149] K. Fine. Semantics for quantified relevance logic. Journal of Philosophical Logic,17(1), 1988
[150] X. Wu, J. G. Sun, K. Hou. Extension rule in first order logic. In: Proc. of 5th International Conference on Cognitive Informatics (ICCI 2006), Beijing, China, 2006,pp.701-706
[151] H. Lin, J. G. Sun, Y. M. Zhang. Theorem proving based on extension rule. Journal of Automated Reasoning, Springer, Berlin, 31: 11-21,2003
[152] X.Wu, J.G.Sun, K.Hou. An extension rule based first-order theorem proven In:Proc. of 1st International Conference on Knowledge Science, Engineering and Management(KSEM 2006), Guilin, China, 2006, pp.514-524
[153] X.Wu, J.G.Sun, S.Lu et al. Improved propositional extension rule. In:Proc. of 1st International Conference on Rough Sets and Knowledge Technology(RSKT2006),Chongqing, China, 2006, pp.592-597
[154] J. N. Hooker, G. Rago, V. Chandru, A. Shrivastava. Partial instantiation methods for inference in first-order Logic. Journal of Automated Reasoning, 28: 371-396,2002
[155] H. Ganzinger, 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, 55-64, 2003
[156] L. Wos et al. Automated Reasoning: Introduction and Applications. McGraw-Hill,New York, 1992
[157] C. Walther. A mechanical solution of Schubert's Streamroller by many-sorted resolution. Aritificial Intelligence, 26(2): 217-224, 1986
[158] A. G. Hamilton. Logic for Mathematicians. Tsinghua University Press, 2003
[159] R. Zabel. Proof theory of finite-valued logics. [PH D dissertation]. Institut for Algebra and Diskrete Mathematic, TU Wien, 1993