【摘 要】
：
Using the interactive theorem proving tool Coq,we completed the construction of the machine proving system of the axiomatic set theory.The axiomatic set theory used in this paper refers to Kelleys axi
【机 构】
：
Beijing Key Laboratory of Work Safety Intelligent Monitoring,School of Electronic Engineering Beijin
论文部分内容阅读
Using the interactive theorem proving tool Coq,we completed the construction of the machine proving system of the axiomatic set theory.The axiomatic set theory used in this paper refers to Kelleys axiomatic set theory.Kelleys axiomatic set theory is based on eight axioms and one axiom scheme,and it is free from the more obvious paradoxes.The system we developed has completed the proof of Kelleys axiomatic set theory with Coq,including the description of eight axioms and one axiom schema and the description or proof of all 181 definitions or theorems with Coq.The proving process demonstrates that the Coq-based machine proving of mathematics theorem is highly readable,interactive,rigorous and reliable.
其他文献
The photoelectric conversion efficiency of photovoltaic cells is mainly affected by temperature and irradiance,in order to promote the development of photovoltaic power generation,it is necessary to i
The leader-following consensus of multi-agent systems with general linear models is investigated in this paper.The event-based impulsive control protocol and the triggering function based on the state
柔性机械臂的振动会显著降低其定位精度和工作效率.为了对柔性机械臂的振动实施控制,本文提出了一种基于增强学习的模糊控制(增强学习模糊控制,RLFC)方法.增强学习模糊控制方法由增强学习算法和模糊推理系统组成.增强学习算法可以在没有导师信号和预先训练数据的情况下自律的进行学习.它通过与被控对象交互来学习模糊规则库,并通过计算回报函数信号来改变规则库生成策略来实现学习目标.为了验证提出的控制方法,本文考
内河集装箱班轮由于船体结构小,更强调舱容利用率,且船舶配载计划脆性极强.内河集装箱班轮航线配载决策需要制定航线各港口配载计划,港口配载计划包含主贝计划和贝内计划.本文采用多阶段分层决策方法进行航线配载智能决策,多港口对应多阶段决策,各港口配载决策中设计贪婪随机自适应搜索优化上层主贝计划,启发式演化策略算法优化下层贝内计划.基于真实场景算例研究表明,该优化算法可以有效求解内河集装箱班轮航线配载问题.
本文从数字智能化时代内外部环境对高校财务管理提出的新要求出发,提出构建高校财务云平台的价值、思路、关键建设点及具体实施路径。
智慧城市提出10年以来,依然存在概念不清晰,顶层设计缺乏,信息孤岛等问题,随着互联网的进一步发展,互联网类脑架构越来越清晰,作为城市建筑与互联网结合的产物,智慧城市也将出现新的架构,城市云脑由此产生,基于互联网云脑,本文重点阐述了如何通过类脑组织形式建设智慧城市,并依托大社交网络(城市神经网络)和城市云反射弧对智慧城市建设水平(城市智商)进行评价.
This paper is concerned with the state consensus for double-integrator heterogeneous networks based on asynchronous periodic edge-event-triggered control.This paper considers the practical scenario: 1
现今仿真模型重用问题仍然是仿真领域最具挑战性的四个研究领域之一,关于模型重用的研究仍然面临缺乏理论支撑问题,而在基础理论研究方面,对模型重用的全生命周期系统化的、规范化的研究尤为重要.本文从仿真模型重用的全生命周期角度出发,建立了面向全生命周期的仿真模型重用过程模型,并结合云计算、云仿真等技术给出了在云环境下模型重用服务的全生命周期,力求规范仿真模型重用过程并指导仿真参与人员,以对模型重用过程理解
利用交互式定理证明工具Coq,在公理化集合论体系下,给出选择公理与它的几个著名等价命题间等价性的机器证明,这些命题包括Tukey引理、Hausdorff最大原则、最大原则、Zorn引理、良序原则等.本文从选择公理出发依次证明上述定理,最后又通过良序原则证明了选择公理,从而循环证明了选择公理与这些命题间的等价性.本文体现了基于Coq的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可