【摘 要】
：
可计算性（Computability）即算法有解性,是数学和计算机科学领域中重要的概念之一。可计算性逻辑（Computability Logic,CoL）是关于可计算性的形式理论,是一种交互的资源逻辑。其中
【基金项目】
：
国家自然科学基金项目（61202014）资助
论文部分内容阅读
可计算性（Computability）即算法有解性,是数学和计算机科学领域中重要的概念之一。可计算性逻辑（Computability Logic,CoL）是关于可计算性的形式理论,是一种交互的资源逻辑。其中,CoL2系统采用博弈的语义,是对经典命题逻辑的扩展,在经典命题逻辑的基础上添加了选择运算和一般原子,比经典命题逻辑更富有表达力,具有更广阔的应用前景,并且有较高的证明效率。分析了CoL2系统的可判定性,即通过提出一个算法来判断任意一个CoL2公式是否是可证明的,并且证明了该算法是多项式空间内运行的。
其他文献
采用钻爆法修建小间距隧道时,后行隧道爆破施工将对先行隧道结构产生振动,影响先行隧道的安全性。以北京怀柔区头道穴小间距隧道为工程背景,采用ANSYS软件建立二维数值计算模
由于北京多条高速公路和高速铁路建设全面铺开,促使隧道爆破技术迅猛发展。针对隧道爆破工程地处偏远、爆破作业频繁、作业环境差,爆炸物品的配送和储存与露天爆破大不相同,
恶意PDF文档依然是网络安全中的威胁,甚至造成了许多重大的安全事故。现有检测方法主要分析恶意代码提取及仿真执行两个方面,检测效率不高,缺乏对PDF文档的针对性。在分析PDF
可转换代理签密算法具有保护用户隐私、抗重放攻击、抗抵赖性等优势,基于该算法提出一种SAML跨域单点登录协议（SSPCPS）。通过用户与异构域服务器直接交互认证,简化了跨域单点登
能量捕获无线传感器网络是无源感知技术中非常重要的一类,它能够有效解决节点能量受限的问题,保持网络运行的持续性。现有的路由方法并未充分利用节点的能量捕获特性,也没有
基于属性的访问控制模型（ABAC）特别适用于大规模分布式网络。然而,由于网络环境的异构性以及策略控制的复杂性,其访问控制策略集往往庞大且缺乏统一语义,策略管理也因此变得复
网页主题挖掘对自然语言处理如网页文本分类、文摘自动生成、信息融合等具有重要意义。挖掘网页主题可以帮助用户更好地理解网页内容。尽管已有一些从普通文本中挖掘概念的工