Computer Science ›› 2021, Vol. 48 ›› Issue (11A): 669-671.doi: 10.11896/jsjkx.210200012

• Interdiscipline & Application • Previous Articles     Next Articles

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

CLC Number: 

  • 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] ZHAO Lu, YUAN Li-ming, HAO Kun. Review of Multi-instance Learning Algorithms [J]. Computer Science, 2022, 49(6A): 93-99.
[2] WANG Yi-jie, XU Yang, WU Guan-feng. Branching Heuristic Strategy Based on Learnt Clauses Deletion Strategy for SAT Solver [J]. Computer Science, 2021, 48(11): 294-299.
[3] SUN Xiao-xiang, CHEN Zhe. Study on Correctness of Memory Security Dynamic Detection Algorithm Based on Theorem Proving [J]. Computer Science, 2021, 48(1): 268-272.
[4] SHEN Xue, CHEN Shu-wei, AI Sen-yang. Reward Mechanism Based Branching Strategy for SAT Solver [J]. Computer Science, 2020, 47(7): 42-46.
[5] LIU Jiang, ZHOU Hong-hao. New Algebraic Logic Reduction Method for Boolean Formula [J]. Computer Science, 2020, 47(5): 32-37.
[6] CAO Feng,XU Yang,ZHONG Jian,NING Xin-ran. First-order Logic Clause Set Preprocessing Method Based on Goal Deduction Distance [J]. Computer Science, 2020, 47(3): 217-221.
[7] FAN Yong-qian, CHEN Gang, CUI Min. Formalization of Finite Field GF(2n) Based on COQ [J]. Computer Science, 2020, 47(12): 311-318.
[8] LIU Ting, XU Yang, CHEN Xiu-lan. Unit Clauses and Their Complementary Literals and Redundant Clauses in Propositional Logic [J]. Computer Science, 2019, 46(8): 255-259.
[9] MA Zhen-wei,CHEN Gang. Matrix Formalization Based on Coq Record [J]. Computer Science, 2019, 46(7): 139-145.
[10] LIU Ji-qin , ZHANG Hai-yue. Information P-dependence and P-dependence Mining-sieving [J]. Computer Science, 2018, 45(7): 202-206.
[11] LIU Jing-lei, LIAO Shi-zhong. Complexity of CP-nets Learning [J]. Computer Science, 2018, 45(6): 211-215.
[12] QIAN Jiang, WANG Fan and GUO Qing-jie. Bivariate Non-tensor-product-typed Continued Fraction Interpolation [J]. Computer Science, 2018, 45(3): 83-91.
[13] NI Ying-bo, CHEN Yuan-yan, YE Juan, WANG Ming. Improvement of DV-Hop Algorithm Based on Multiple Communication Radii and Cosine Theorem [J]. Computer Science, 2018, 45(11A): 320-324.
[14] ZHU Shu-qin and LI Jun-qing. Image Encryption Scheme Based on Chaos with Parameter Perturbation [J]. Computer Science, 2017, 44(Z6): 356-360.
[15] LU Juan and LI De-yu. Model for Type-2 Fuzzy Rough Attribute Reduction [J]. Computer Science, 2017, 44(9): 28-33.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!