计算机科学 ›› 2021, Vol. 48 ›› Issue (11A): 669-671.doi: 10.11896/jsjkx.210200012
郝娇, 惠小静, 马硕, 金明慧
HAO Jiao, HUI Xiao-jing, MA Shuo, JIN Ming-hui
摘要: 一阶逻辑是公理系统的标准形式逻辑之一,其中包含的程度化推理等研究内容,是一个研究热点也是难点。文中从一阶逻辑演算的语义理论出发,利用可满足性及完备性定理研究了一阶逻辑中公理化真度。首先给出并、交运算可满足性的定义,其次说明了两个特殊公式与逻辑有效公式以及定理的关系,最后得出与公式等价的前束范式。上述结果将为谓词逻辑程度化研究做准备。
中图分类号:
[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 |
|