计算机科学 ›› 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
  • 基金资助:
    国家自然科学基金项目(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.

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] 王钇杰, 徐扬, 吴贯锋.
基于学习子句删除策略的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   
No Suggested Reading articles found!