计算机科学 ›› 2021, Vol. 48 ›› Issue (11A): 669-671.doi: 10.11896/jsjkx.210200012

• 交叉& 应用 • 上一篇    下一篇


郝娇, 惠小静, 马硕, 金明慧   

  1. 延安大学数学与计算机科学学院 陕西 延安716000
  • 出版日期:2021-11-10 发布日期:2021-11-12
  • 通讯作者: 惠小静(xhmxiaojing@163.com)
  • 作者简介:825716511@qq.com
  • 基金资助:

Study on Axiomatic Truth Degree in First-order Logic

HAO Jiao, HUI Xiao-jing, MA Shuo, JIN Ming-hui   

  1. School of Mathematics and Computer Science,Yan'an University,Yan'an,Shaanxi 716000,China
  • Online:2021-11-10 Published:2021-11-12
  • About author:JIANG Hua-nan,born in 1988,master.His main research interests include high-performance computing,robotics and finite element simulation.
    ZHANG Shuai,born in 1986,Ph.D.His main research interests include robotics and CFD simulation.
  • Supported by:
    National Natural Science Foundation of China(11471007,61763045),National Innovation and Entrepreneurship Training Program for College Students(201910719023) and Postgraduate Education Reform Research Project of Yan'an University(YDYJG2018022,YDYJG2017024).

摘要: 一阶逻辑是公理系统的标准形式逻辑之一,其中包含的程度化推理等研究内容,是一个研究热点也是难点。文中从一阶逻辑演算的语义理论出发,利用可满足性及完备性定理研究了一阶逻辑中公理化真度。首先给出并、交运算可满足性的定义,其次说明了两个特殊公式与逻辑有效公式以及定理的关系,最后得出与公式等价的前束范式。上述结果将为谓词逻辑程度化研究做准备。

关键词: 定理, 可满足性, 逻辑有效公式, 前束范式, 一阶逻辑

Abstract: First-order logic,as one of the standard formal logics of axiomatics systems,contains the research contents such as degree reasoning,which is a hot and difficult point.Based on the semantic theory of first-order logic calculus,this paper studies the axiomatic truth degree of first-order logic by using the satisfiability and completeness theorem.Firstly,the definition of the satisfiability of union and intersection operation is given.Secondly,the relationship between two special formulas and logical effective formulas and theorems is explained.Finally,the prenex normal form equivalent to formulas is obtained.The above results will prepare for the research of predicate logic degree.

Key words: First-order logic, Logically valid formula, Prenex normal form, Satisfiability, Theorem


  • O141
[1]REN F J,SUN X.Present Situation and Development of Intelligent Robots[J].Science & Technology Review,2015,33(21):32-38.
[2]LIU Y,XU H,GENG C X,et al.Research on Manipulator Motion Planning in ROS/Gazebo[J].Coal Mine Machinery,2018,39(3):42-44.
[3]YAO W J.Distributed Multi-robot Circumnavigation Formation Control[D].Changsha:National University of Defense Technology,2017.
[4]CHEN X,XIA Y C,HUANG X H.A Digital Hard-in-the-Loop Real Time Simulation System for Flight Control[J].Journal of Nanjing University of Aeronautics & Astronautics,2001,33(2):200-203.
[5]ZHAO Z J,ZHONG S J,LI J L,et al.Ground Simulation ofUVA Flight Control[J].Ordnance Industry Automation,2013,32(8):32-34.
[6]JIANG Y,YUANG M T.Construction of Robot Flexible Operation Control Platform Based on Gazebo[J].Industrial Control Computer,2018,31(12):44-46.
[7]TAN Z.Some Problems in Formation Control of Quadrotor[D].Hangzhou:Hangzhou Dianzi University,2019.
[8]HAO P P,YAO L F.Mobile Robot Path Planning Simulation based on Player/Gazebo[J].Education Circle,2010(10):138.
[9]ZHANG J W,ZHANG L W,HU Y,et al.Open source operating system-ROS[M].Beijing:Science Press,2012.
[10]XIE M.Vehicle remote control and navigation simulation based on ROS[D].Hefei:University of Science and Technology,2019.
[11]WANG D G,WANG B H.Seven-degree-of-freedom robot arm Simulation and Motion Planning based on ROS[J].Science and Technology & Innovation,2018(2):116-117.
[12]QUIGLEY M,CONLEY K,GERKEY B P,et al.ROS:an open-source Robot Operating System[C] //ICRA Workshop on Open Source Software.2009.
[13]YU W L.A Mapping Simulation Design of Mobile RobotSLAM Based on ROS[J].Software Engineering and Applications,2020,9(4):294-301.
[14]FAN P Q,ZHANG L,TANG S,et al.Impletmentation andPerformance Analysis of MPI+Open MPI Hybrid Programming[J].Computer Science and Application,2019,9(10):1859-1866.
[15]ZHANG Z H.The Study of Parallel Computing Based on MPI[D].Beijing:China University of Geosciences,2006.
[1] 赵璐, 袁立明, 郝琨.
Review of Multi-instance Learning Algorithms
计算机科学, 2022, 49(6A): 93-99. https://doi.org/10.11896/jsjkx.210500047
[2] 王钇杰, 徐扬, 吴贯锋.
Branching Heuristic Strategy Based on Learnt Clauses Deletion Strategy for SAT Solver
计算机科学, 2021, 48(11): 294-299. https://doi.org/10.11896/jsjkx.201000142
[3] 孙小祥, 陈哲.
Study on Correctness of Memory Security Dynamic Detection Algorithm Based on Theorem Proving
计算机科学, 2021, 48(1): 268-272. https://doi.org/10.11896/jsjkx.200100097
[4] 沈雪, 陈树伟, 艾森阳.
Reward Mechanism Based Branching Strategy for SAT Solver
计算机科学, 2020, 47(7): 42-46. https://doi.org/10.11896/jsjkx.190700191
[5] 刘江, 周鸿昊.
New Algebraic Logic Reduction Method for Boolean Formula
计算机科学, 2020, 47(5): 32-37. https://doi.org/10.11896/jsjkx.190400018
[6] 曹锋,徐扬,钟建,宁欣然.
First-order Logic Clause Set Preprocessing Method Based on Goal Deduction Distance
计算机科学, 2020, 47(3): 217-221. https://doi.org/10.11896/jsjkx.190100004
[7] 范永乾, 陈钢, 崔敏.
Formalization of Finite Field GF(2n) Based on COQ
计算机科学, 2020, 47(12): 311-318. https://doi.org/10.11896/jsjkx.190900197
[8] 刘婷, 徐扬, 陈秀兰.
Unit Clauses and Their Complementary Literals and Redundant Clauses in Propositional Logic
计算机科学, 2019, 46(8): 255-259. https://doi.org/10.11896/j.issn.1002-137X.2019.08.042
[9] 马振威,陈钢.
Matrix Formalization Based on Coq Record
计算机科学, 2019, 46(7): 139-145. https://doi.org/10.11896/j.issn.1002-137X.2019.07.022
[10] 刘纪芹, 张海月.
Information P-dependence and P-dependence Mining-sieving
计算机科学, 2018, 45(7): 202-206. https://doi.org/10.11896/j.issn.1002-137X.2018.07.035
[11] 刘惊雷, 廖士中.
Complexity of CP-nets Learning
计算机科学, 2018, 45(6): 211-215. https://doi.org/10.11896/j.issn.1002-137X.2018.06.038
[12] 钱江,王凡,郭庆杰.
Bivariate Non-tensor-product-typed Continued Fraction Interpolation
计算机科学, 2018, 45(3): 83-91. https://doi.org/10.11896/j.issn.1002-137X.2018.03.014
[13] 尼迎波, 陈元琰, 叶娟, 王明.
Improvement of DV-Hop Algorithm Based on Multiple Communication Radii and Cosine Theorem
计算机科学, 2018, 45(11A): 320-324.
[14] 朱淑芹,李俊青.
Image Encryption Scheme Based on Chaos with Parameter Perturbation
计算机科学, 2017, 44(Z6): 356-360. https://doi.org/10.11896/j.issn.1002-137X.2017.6A.081
[15] 路娟,李德玉.
Model for Type-2 Fuzzy Rough Attribute Reduction
计算机科学, 2017, 44(9): 28-33. https://doi.org/10.11896/j.issn.1002-137X.2017.09.005
Full text



No Suggested Reading articles found!