• 交叉& 应用 •

一阶逻辑中公理化真度研究

1. 延安大学数学与计算机科学学院 陕西 延安716000
• 出版日期:2021-11-10 发布日期:2021-11-12
• 通讯作者: 惠小静(xhmxiaojing@163.com)
• 作者简介:825716511@qq.com
• 基金资助:
国家自然科学基金项目(11471007,61763045);国家级大学生创新创业训练计划项目(201910719023);延安大学研究生教改研究项目(YDYJG2018022,YDYJG2017024)

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.

• 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] 王钇杰, 徐扬, 吴贯锋. 基于学习子句删除策略的SAT求解器分支策略 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] 沈雪, 陈树伟, 艾森阳. 基于奖励机制的SAT求解器分支策略 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] 范永乾, 陈钢, 崔敏. 基于COQ的有限域GF(2n)的形式化研究 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] 马振威,陈钢. 基于Coq记录的矩阵形式化方法 Matrix Formalization Based on Coq Record 计算机科学, 2019, 46(7): 139-145. https://doi.org/10.11896/j.issn.1002-137X.2019.07.022 [10] 刘纪芹, 张海月. 信息的P-依赖与信息P-依赖挖掘-筛选 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] 刘惊雷, 廖士中. CP-nets学习的复杂度 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] 尼迎波, 陈元琰, 叶娟, 王明. 基于多通信半径加余弦定理的DV-Hop算法的改进 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
Viewed
Full text

Abstract

Cited

Shared
Discussed