• ISSN 0258-2724
  • CN 51-1277/U
  • EI Compendex
  • Scopus
  • Indexed by Core Journals of China, Chinese S&T Journal Citation Reports
  • Chinese S&T Journal Citation Reports
  • Chinese Science Citation Database
Volume 55 Issue 3
Jun.  2020
Turn off MathJax
Article Contents
Abstract
References
Journal of Southwest Jiaotong University  > 2020  >  55(3): 588-595.
NING Xinran, XU Yang, HE Xingxing. Extended Unifying Principle of Clause Elimination in First-Order Logic[J]. Journal of Southwest Jiaotong University, 2020, 55(3): 588-595. doi: 10.3969/j.issn.0258-2724.20180974
Citation: NING Xinran, XU Yang, HE Xingxing. Extended Unifying Principle of Clause Elimination in First-Order Logic[J]. Journal of Southwest Jiaotong University, 2020, 55(3): 588-595. doi: 10.3969/j.issn.0258-2724.20180974
shu

Extended Unifying Principle of Clause Elimination in First-Order Logic

doi: 10.3969/j.issn.0258-2724.20180974
  • Received Date: 27 Nov 2018
  • Rev Recd Date: 18 Jun 2019
    • Available Online: 30 Mar 2020
  • Publish Date: 01 Jun 2020
    Abstract
  • Simplifications are indispensable steps of first-order theorem proving, which can enhance the proving efficiency of first-order theorem provers. Set implication modulo resolution, a principle of identifying the redundancy property of clauses, is proposed. The soundness of this principle in first-order logic without equality is proved, which means that eliminating clauses according to the principle has not effect on the unsatisfiability or satisfiability of original formulas. In addition, two novel preprocessing methods in first-order theorem proving are developed given the principle of set implication modulo resolution, i.e., set resolution subsumption elimination (SRSE) and set resolution asymmetric tautology elimination (SRATE). The soundness of the two clause elimination methods is also demonstrated. Finally, the effectiveness is theoretically compared between SRSE and resolution subsumption elimination (RSE) and between SRATE and resolution asymmetric tautology elimination (RATE), which shows SRSE and SRATE are more effective than RSE and RATE, respectively.

     

    • FullText(HTML)
    • References(21)
  • MENEGUZZI F, TELANG P, SINGH M. A first-order formalization of commitments and goals for planning[C]//Proceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence. Bellevue: AAAI Press, 2013: 697-703.
    MORITOMO A, HAMAGUCHI K, KASHIWABARA T. Validity checking for quantifier-free first-order logic with equality using substitution of boolean formulas[C]//International Symposium on Automated Technology for Verification and Analysis 2004, Lecture Notes in Computer Science. Berlin: Springer, 2004: 108-119.
    BECKERT B, HAHNLE R. Reasoning and verification:state of the art and current trends[J]. IEEE Intelligent Systems, 2014, 29(1): 20-29. doi: 10.1109/MIS.2014.3
    GRUNINGER M, HULL R, MCILRAITHS A. Short overview of flows: a first-order logic ontology for web services[C]//Bulletin of the IEEE Computer Society Technical Committee on Data Engineering. [S.l.]: IEEE, 2008: 3-7.
    WITHERELL P, KRISHNAMURTY S, GROSSE I, et al. Improved knowledge management through first-order logic in engineering design ontologies[J]. Creativity:Simulation,Stimulation,and Studies, 2010, 24(2): 245-257.
    WANG Zhenghao, YAN Shengquan, WANG Huaming, et al. An overview of Microsoft deep QA system on stanford web questions benchmark[R]. Washington D. C.: Microsoft, 2014.
    HODER K, VORONKOV A. Sine qua non for large theory reasoning[C]//Automated Deduction-CADE-23. [S.l.]: CADE, 2011: 299-314.
    ALAMA J, HESKES, T, KUHLWEIN D, et al. Premise selection for mathematics by corpus analysis and kernel methods[J]. Journal of Automated Reasoning, 2014, 52: 191-213. doi: 10.1007/s10817-013-9286-5
    KHASIDASHVILI Z, KOROVIN K. Predicate elimination for preprocessing in first-order theorem proving[C]//International Conference on Theory and Applications of Satisfiability Testing, Lecture Notes in Computer Science. [S.l.]: SAT, 2016: 361-372.
    KIESL B, SUDA M, SEIDL M. et al. Blocked clauses in first-order logic[C/OL]//Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21). [2018-09-20]. https://arxiv.org/pdf/1702. 00847.pdf.
    NING Xinran, XU Yang; WU Guanfeng, et al. Set-blocked clause and extended set-blocked clause in first-order logic[J]. Symmetry, 2018, 10: 533-1-533-15.
    BLOCKEEL H. Identifying non-redundant literals in clauses with uniqueness propagation[C]//The 26th International Conference on Inductive Logic Programming. [S.l.]: Springer, 2017: 8-13.
    PIOTROWSKI P, URBAN J. ATPboost: learning premise selection in binary setting with ATP feedback[EB/OL]. [2018-2-15]. https://arxiv.org/abs/1802.03375?context=stat.
    KUHLWEIN D, BLANCHETTE J. C. A survey of axiom selection as a machine learning problem[R]. Infinity, Computability and Metamathematics: Festschrift celebrating the 60th birthdays of Peter Koepke and Philip Welch. London: [s.n.], 2014.
    陈青山,徐扬,何星星. 利用逻辑演绎求解SAT问题的启发式完全算法[J]. 西南交通大学学报,2017,52(6): 1224-1232. doi: 10.3969/j.issn.0258-2724.2017.06.025

    CHEN Qingshan, XU Yang, HE Xingxing. Heuristic complete algorithm for SAT problem by using logical deduction[J]. Journal of Southwest Jiaotong University, 2017, 52(6): 1224-1232. doi: 10.3969/j.issn.0258-2724.2017.06.025
    KIESL B, SUDA M. A unifying principle for clause elimination in first-order logic[C]//International Conference on Automated Deduction, Lecture Notes in Computer Science. [S.l.]: Springer, 2017: 274-290.
    HEULE M J H, JARVISALO M, BIERE A. Covered clause elimination[C]//Short Papers for the 17th International Conference on Logic for Programming, Artificial intelligence, and Reasoning (LPAR-17-short). Yogyakarta: [s.n.], 2010, 13: 41-46.
    HEULE M J H, JARVISALO M, BIERE A. Clause elimination procedures for CNF formulas[C]//Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17). [S.l.]: Springer, 2010: 357-371
    JARVISALO M, HEULE M J H, BIERE A. Inprocessing rules[C]//International Joint Conference on Automated Reasoning. [S.l.]: Springer, 2012: 355-370
    刘叙华. 基于归结方法的自动推理[M]. 北京: 科学出版社, 1994.
    HEULE M J H, SEIDL M, BIERE A. Solution validation and extraction for QBF preprocessing[J]. Journal of Automated Reasoning, 2017, 58: 1-29. doi: 10.1007/s10817-016-9394-0
    • Relative Articles

  • Relative Articles

    [1]ZENG Guoyan, XU Yang, CHEN Shuwei, JIANG Shipan. First-Order Logic Clause Selection Method Based on Multi-criteria Decision Making[J]. Journal of Southwest Jiaotong University, 2025, 60(1): 185-193. doi: 10.3969/j.issn.0258-2724.20230023
    [2]XU Xianze, SONG Mingxing, GONG Yongxing, XU Fengqiu, WANG Dijin, SUI Bowen, GUO Qingquan. Fractional-Order Sliding Mode Control for Maglev Rotary Table Based on Disturbance Compensation[J]. Journal of Southwest Jiaotong University, 2024, 59(4): 766-775. doi: 10.3969/j.issn.0258-2724.20230412
    [3]LIU Qinghua, LI Ruijie, ZHU Xusheng, CHEN Daixin. First-Order Logical Premise Selection Method Based on Symbol Weight[J]. Journal of Southwest Jiaotong University, 2023, 58(3): 704-710. doi: 10.3969/j.issn.0258-2724.20220478
    [4]LIU Qinghua, XU Yang, WU Guanfeng, LI Ruijie. Edge-Weighted-Based Graph Neural Network for First-Order Premise Selection[J]. Journal of Southwest Jiaotong University, 2022, 57(6): 1368-1375. doi: 10.3969/j.issn.0258-2724.20210134
    [5]CAO Feng, XU Yang, CHEN Shuwei, WU Guanfeng, CHANG Wenjing. Application of Multi-Clause Synergized Deduction in First-Order Logic Automated Theorem Proving[J]. Journal of Southwest Jiaotong University, 2020, 55(2): 401-408, 427. doi: 10.3969/j.issn.0258-2724.20180800
    [6]SUN Shibao, QIN Keyun. Construction Method of Fuzzy Concept Lattices Based on Residual Implication[J]. Journal of Southwest Jiaotong University, 2006, 19(2): 259-263.
    [7]PANXiao-dong, XU Yang, ZHANG Qing. Lattice Implication Algebraic Equations in Lattice Implication Algebras[J]. Journal of Southwest Jiaotong University, 2005, 18(6): 842-845.
    [8]WANG Wei, JIANG Bao-qing, XU Yang. α-Resolution Fields ofGeneralized Literals ofLogic LP(X)[J]. Journal of Southwest Jiaotong University, 2005, 18(4): 544-547.
    [9]QIN Ke-yun, TU Wen-biao. Rough Set Algebra and Lattice Implication Algebra[J]. Journal of Southwest Jiaotong University, 2004, 17(6): 754-757.
    [10]MAJun, GAO Ya, QINKe-yun, XUYang. Syntactic System of Lattice-Valued Propositional Logic Based on Finite Lattice Implication Algebra[J]. Journal of Southwest Jiaotong University, 2004, 17(1): 90-94.
    [11]WANG Qiong, HE Yi-nong, SONG Zhen-min. Sustaining Degree of Fuzzy Triple I Method Based on Residual Implication[J]. Journal of Southwest Jiaotong University, 2004, 17(4): 550-553.
    [12]WANG Wei, XUYang, QINKe-yun. The Topological Structure of Lattice Implication Algebras[J]. Journal of Southwest Jiaotong University, 2002, 15(3): 343-346.
    [13]PEI Zheng, HUANG Tian-min. Input Resolution on Horn Sets Based on Fuzzy Neural Networks[J]. Journal of Southwest Jiaotong University, 2002, 15(5): 565-569.
    [14]MAJun, QIN Ke-yun, XU Yang. Semantic System of Lattice-Valued Propositional Logic Based on Finite Lattice Implication Algebra[J]. Journal of Southwest Jiaotong University, 2002, 15(5): 557-560.
    [15]QIN Ke-yun, XU Yang. On Model Properties of Lattice Implication Algebra[J]. Journal of Southwest Jiaotong University, 2000, 13(5): 546-550.
    [16]Qin Keyun, Xu Yang. On Ultrafilters of Lattice Implication Algebras[J]. Journal of Southwest Jiaotong University, 1999, 12(1): 52-54.
    • Supplements(0)
    • Cited By

  • Cited by

    Periodical cited type(1)

    1. 曹锋，谢燏，易见兵，李俊. 矛盾体分离单元结果演绎方法及应用. 计算机工程与科学. 2024(12): 2252-2260 .

    Other cited types(0)

  • Created with Highcharts 5.0.7Amount of accessChart context menuAbstract Views, HTML Views, PDF Downloads StatisticsAbstract ViewsHTML ViewsPDF Downloads2024-052024-062024-072024-082024-092024-102024-112024-122025-012025-022025-032025-0302.557.51012.5
    Created with Highcharts 5.0.7Chart context menuAccess Class DistributionFULLTEXT: 38.6 %FULLTEXT: 38.6 %META: 58.9 %META: 58.9 %PDF: 2.5 %PDF: 2.5 %FULLTEXTMETAPDF
    Created with Highcharts 5.0.7Chart context menuAccess Area Distribution其他: 4.7 %其他: 4.7 %上海: 0.8 %上海: 0.8 %临汾: 0.6 %临汾: 0.6 %北京: 5.6 %北京: 5.6 %十堰: 0.3 %十堰: 0.3 %南京: 0.3 %南京: 0.3 %哥伦布: 0.6 %哥伦布: 0.6 %大连: 0.8 %大连: 0.8 %天津: 0.3 %天津: 0.3 %宣城: 0.3 %宣城: 0.3 %广州: 0.6 %广州: 0.6 %张家口: 3.9 %张家口: 3.9 %成都: 5.6 %成都: 5.6 %杭州: 1.1 %杭州: 1.1 %池州: 1.7 %池州: 1.7 %淄博: 0.3 %淄博: 0.3 %漯河: 0.8 %漯河: 0.8 %芒廷维尤: 6.1 %芒廷维尤: 6.1 %芜湖: 0.6 %芜湖: 0.6 %荆门: 0.3 %荆门: 0.3 %衡阳: 0.3 %衡阳: 0.3 %西宁: 60.8 %西宁: 60.8 %西安: 0.6 %西安: 0.6 %贵阳: 0.6 %贵阳: 0.6 %运城: 1.4 %运城: 1.4 %郑州: 0.8 %郑州: 0.8 %长沙: 0.6 %长沙: 0.6 %其他上海临汾北京十堰南京哥伦布大连天津宣城广州张家口成都杭州池州淄博漯河芒廷维尤芜湖荆门衡阳西宁西安贵阳运城郑州长沙

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索
    Get Citation
    PDF
    XML
    Article views(568) PDF downloads(12) Cited by(1)
    Proportional views
    Related

    Copyright © 2009 Journal of Southwest Jiaotong University

    Address: RM449 & 451, Administrative Building, Xipu Campus, Southwest Jiaotong University Western Hi-tech Zone, Chengdu, Sichuan 611756, P. R. China

    Tel: 028-66367562Fax: 028-66366552Email: xbz@home.swjtu.edu.cn

    Supported by: Beijing Renhe Information Technology Co. Ltd  support: info@rhhz.net

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return