• 不 限
  • 期刊论文
  • 硕博论文
  • 会议论文
  • 报 纸
  • 英文论文
  2. 您的位置
  3. 首页
  4. 会议论文
  5. Machine Proving System for Mathematical Theorems in Coq-Machine Proving of Tukey Lemma

Machine Proving System for Mathematical Theorems in Coq-Machine Proving of Tukey Lemma

来源 :2017中国智能物联系统会议 | 被引量 : 0次 | 上传用户：dtj77
【摘 要】
：
Under the axiomatic set theory frame,this paper implements the machine proving of the equivalence between the Axiom of Choice and Tukey lemma using Coq as an interactive theorem proving tool.The provi
【作 者】
：
Sun Tianyu Yu Wensheng 
【机 构】
：
Beijing Key Laboratory of Work Safety Intelligent Monitoring,School of Electronic Engineering Beijin
【出 处】
：
2017中国智能物联系统会议
【发表日期】
：
2017年6期
【关键词】
：
Coq The axiomatic set theory Axiom of Choice Tukey lemma Equivalence Machine pro 
下载到本地 , 更方便阅读
下载此文 赞助VIP
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
　　Under the axiomatic set theory frame,this paper implements the machine proving of the equivalence between the Axiom of Choice and Tukey lemma using Coq as an interactive theorem proving tool.The proving process demonstrates that the Coq-based machine proving of mathematics theorem is highly readable,interactive,rigorous and reliable.
其他文献
Coevolution of nonlinear group interactions and strategies on scale-free networks
From microbial communities to human societies,nonlinear group interactions strongly affect the intraspecific evolutionary dynamics,which leads to the variation of the strategy composition.The conseque
会议
CooperationCoevolutionNonlinear group interactionsEvolutionary dynamics
5W理论下网红直播带货研究 ——以李佳琦为例
学位
Information propagation over signed networks:models and convergence analysis
In this paper,we consider the propagation problem for multiple pieces of information over a network with antagonistic interactions,modeled as a signed graph.The sign attached to an edge in this graph
会议
Signed networkInformation propagationConvergence analysisMulti-agent network
求解多电平变换器特定谐波消除方程组的GPU并行粒子群算法
粒子群算法已经被广泛地用来求解特定谐波消除方程组,但是它在CPU上的执行效率较低,满意满足实际需求.本文将粒子群算法并行化并将其在GPU上运行以提高执行效率.文中使用GPU加速的粒子群算法求解了5到7个不等电平的特定谐波消除方程组,其执行效率比其在CPU上的执行效率高数百倍.通过实验,求解所得开关角的正确性也得到了验证.
会议
多电平变换器谐波消除方程组粒子群算法图形处理器
Mathematical Theorem Machine Proving System Based on Coq -Machine Proving of the Factorization Theor
The complete machine proving of the Factorization Theorem of Principal Ideal Domain in the abstract algebra is given by using the interactive theorem proving tool Coq.The proof process is done by usin
会议
Coqabstract algebraprincipal ideal domainunique factorization ringmachine pr
媒介景观视阈下直播带货表征解读与意义建构 ——以淘宝直播为例
学位
Bipartite Output Tracking of Heterogeneous Linear Multi-agent Systems:LQR-based Approach
In this paper,we consider the bipartite output tracking of heterogeneous linear multi-agent systems with a leader.Negative edge weights are introduced in modelling the communication graph between agen
会议
Multi-agent systemHeterogeneousBipartite output trackingLQR-based approachSt
TVWS Network AP Placement in Indoor 3D Space Based on Path Loss Model
The increasing demand of wireless communication would lead to the scarcity of spectrum resources and many countries and institutions have begun to release rules to use of TV white space(TVWS).Most of
会议
Indoor 3D NetworkAP placement in TVWSWireless Communicate in TVWSPath Loss Mo
Consensus of multi-agent systems via event-triggered model predictive control
This paper considers the consensus problem of multi-agent systems based on event-triggered model predictive control(MPC).By introducing the event-triggering mechanism into MPC,we propose a novel event
会议
Multi-agent systemsconsensusevent-triggered controlmodel predictive control
基于事件驱动和符号网络的多智能体系统一致性研究
本文利用符号网络对一阶线性多智能体系统进行了研究.本文首先介绍了使结构平衡的带符号同构一阶线性多智能体系统实现双边一致性的控制协议,该控制协议需要使系统中智能体之间进行连续的通信,从而实现控制器的相应实时更新.但是在实际的应用中,系统的通信资源都是有限的.为此,本文利用李雅普诺夫函数方法对上述控制协议进行改进,针对于带符号多智能体系统分别提出了集中式和分布式两种基于事件驱动的控制策略.在这样的控制
会议
多智能体系统控制协议双边一致性符号网络事件驱动