检索结果-内蒙古大学图书馆

山东大学学报（理学版） 2011年第9期46卷 22-27页

作者：马艳芳张敏陈仪香淮北师范大学计算机科学与技术学院安徽淮北235000 华东师范大学软件学院上海200062 上海市高可信计算重点实验室上海200062

软件的运行依赖于环境,在考察软件正确性时需要考虑环境的因素。软件在开发和设计过程中,其正确性是一个逐渐改进的过程,也就是说,通过不断地修改,软件越来越接近于正确。为了刻画软件的这种动态正确性并考虑环境的因素,本文将以三分之... 详细信息

软件的运行依赖于环境,在考察软件正确性时需要考虑环境的因素。软件在开发和设计过程中,其正确性是一个逐渐改进的过程,也就是说,通过不断地修改,软件越来越接近于正确。为了刻画软件的这种动态正确性并考虑环境的因素,本文将以三分之二互模拟为基础,利用网极限的观点,建立软件动态正确性的形式化描述。首先建立三分之二互模拟的无限演化理论,给出三分之二极限互模拟的定义。其次建立三分之二互模拟极限,这个极限在一定程度上反映软件规范是其实现的极限形式。最后证明三分之二互模拟极限与三分之二互模拟的相容性等性质。

关键词：极限三分之二互模拟正确性形式化

来源：评论

学校读者我要写书评

暂无评论

常用基本不等式的机器证明

引用

智能系统学报 2011年第5期6卷 377-390页

作者：杨路郁文生华东师范大学上海高可信计算重点实验室

不等式机器证明问题是智能系统领域的难点和热点问题.借助不等式证明软件BOTTEMA,对若干常用的基本不等式成功地实现了机器证明,包括算术、几何与调和平均不等式、排序不等式、Chebyshev不等式、Bernoulli不等式、三角形不等式及Jensen... 详细信息

不等式机器证明问题是智能系统领域的难点和热点问题.借助不等式证明软件BOTTEMA,对若干常用的基本不等式成功地实现了机器证明,包括算术、几何与调和平均不等式、排序不等式、Chebyshev不等式、Bernoulli不等式、三角形不等式及Jensen不等式等.所论不等式含有的变元个数是一个不确定的变量,属于Tarski模型外的不等式类型.机器证明得出的结论有时可能是已知结果的推广,其方法本身对同类不等式有示范性,更多的例子表明了该算法和软件的有效性.

关键词：基本不等式机器证明不等式证明软件BOTTEMA Tarski模型

来源：评论

学校读者我要写书评

暂无评论

线性系统的同时镇定问题

引用

控制理论与应用 2011年第1期28卷 1-12页

作者：关强何冠男王龙郁文生中国科学院自动化研究所综合信息系统研究中心北京化工大学信息科学与技术学院北京大学工学院机器感知与智能教育部重点实验室华东师范大学上海高可信计算重点实验室

线性系统的同时镇定问题,是系统与控制理论中的基本问题,有着广泛的理论意义和应用价值.本文介绍了线性系统同时镇定问题的研究现状和最新进展.首先回顾了同时镇定问题的研究内容、基本方法及相关结果.其次,从理论求解和控制器设计的角... 详细信息

线性系统的同时镇定问题,是系统与控制理论中的基本问题,有着广泛的理论意义和应用价值.本文介绍了线性系统同时镇定问题的研究现状和最新进展.首先回顾了同时镇定问题的研究内容、基本方法及相关结果.其次,从理论求解和控制器设计的角度对线性系统同时镇定研究中著名的"香槟问题","比利时巧克力问题"和"威士忌问题"进行了分析探讨,并基于不等式型定理机器证明理论,给出了线性系统同时镇定问题的相关工作.最后指出了对于同时镇定多个线性系统方面的若干研究方向.

关键词：线性系统同时镇定香槟问题比利时巧克力问题威士忌问题复分析不等式型定理机器证明半代数系统

来源：评论

学校读者我要写书评

暂无评论

逻辑系统MTL_▽及其完备性

引用

计算机工程与应用 2011年第6期47卷 30-33页

作者：时慧娴王国俊陕西师范大学数学与信息科学学院西安710062 华东师范大学上海市高可信计算重点实验室上海200062

在逻辑系统MTL(Monoidal t-norm based Logic)中引入一元逻辑连接词▽,并在原有公理模式的基础上添加若干新公理,构建了一种新的MTL的扩张MTL▽逻辑系统。为了进行相应的语义研究,在MTL代数的基础上,引入一元算子▽,提出MTL▽代数的概念... 详细信息

在逻辑系统MTL(Monoidal t-norm based Logic)中引入一元逻辑连接词▽,并在原有公理模式的基础上添加若干新公理,构建了一种新的MTL的扩张MTL▽逻辑系统。为了进行相应的语义研究,在MTL代数的基础上,引入一元算子▽,提出MTL▽代数的概念,并证明了MTL▽代数的同构定理。基于线性MTL▽代数证明了逻辑系统MTL▽的完备性。

关键词： MTL↓△逻辑系统 MTL↓△代数完备性扩张

来源：评论

学校读者我要写书评

暂无评论

面向不确定图的k最近邻查询

面向不确定图的k最近邻查询

引用

第28届中国数据库学术会议

作者：张旭何向南金澈清周傲英华东师范大学软件学院上海市高可信计算重点实验室上海200062

生物网络、社会网络、交际网络等复杂的网络被广泛的研究,由于数据抽出时引入的噪声和错误使这些数据具有不确定性,因此可以对这些应用使用不确定图模型建模,k最近邻查询问题是查询一个图上的距离某个特定点最近的k个邻居节点的问题,它... 详细信息

生物网络、社会网络、交际网络等复杂的网络被广泛的研究,由于数据抽出时引入的噪声和错误使这些数据具有不确定性,因此可以对这些应用使用不确定图模型建模,k最近邻查询问题是查询一个图上的距离某个特定点最近的k个邻居节点的问题,它是不确定图上的一个基础问题。设计了一个解决不确定图上最近邻问题的框架,首先定义了一种新颖的不确定图上的k最近邻查询,然后提出了针对该查询的一般处理算法,同时对该算法进行了优化,使算法效率得到极大提高。理论分析和实验结果表明提出的算法能够高效地处理不确定图上的k最近邻查询。

关键词：数据挖掘信息处理不确定图 k最近邻查询算法效率

来源：评论

学校读者我要写书评

暂无评论

特定消谐脉宽调制开关角度的实解个数

引用

中国矿业大学学报 2011年第5期40卷 766-773页

作者：杨克虎袁如意项勇郁文生中国矿业大学(北京)机电与信息工程学院北京100083 中国科学院自动化研究所综合信息中心北京100190 奥大利亚迪肯大学工程学院维多利亚吉朗3217 华东师范大学上海高可信计算重点实验室上海200062

为了解决特定消谐脉宽调制技术中开关角度非线性超越方程组的实解个数问题,利用三角函数倍角公式将非线性超越方程组转化为带不等式约束的多项式方程组,提出了一种基于半代数系统机器证明算法的实解分类方法.给出了N=3时的单相和三相逆... 详细信息

为了解决特定消谐脉宽调制技术中开关角度非线性超越方程组的实解个数问题,利用三角函数倍角公式将非线性超越方程组转化为带不等式约束的多项式方程组,提出了一种基于半代数系统机器证明算法的实解分类方法.给出了N=3时的单相和三相逆变器以及N=4时的单相逆变器开关角度实解个数的完全分类,同时首次得到了分类边界点的解析解.理论推导和实验仿真结果表明:该方法能够从理论上给出调制比和实解个数之间的变化关系,对于开关角度的求解以及提高逆变器的消谐效果具有重要的指导意义.

关键词：特定消谐半代数系统脉宽调制逆变器

来源：评论

学校读者我要写书评

暂无评论

计算广告:以数据为核心的Web综合应用

计算广告:以数据为核心的Web综合应用

引用

第28届中国数据库学术会议

作者：周傲英周敏奇宫学庆华东师范大学软件学院上海200062 上海高可信重点实验室上海200062

文中主要介绍计算广告学的演化过程，包括计算广告投放模式的演化、计价模式的演化、投放目标的演化;计算广告学的组成部分，包括计算广告产业链、计算广告的分类。此外，文中还重点讨论了广告检索、排序投放算法以及广告离线分析、实... 详细信息

文中主要介绍计算广告学的演化过程，包括计算广告投放模式的演化、计价模式的演化、投放目标的演化;计算广告学的组成部分，包括计算广告产业链、计算广告的分类。此外，文中还重点讨论了广告检索、排序投放算法以及广告离线分析、实时投放平台等关键技术和平台。最后，还将讨论在移动计算环境下的移动终端的广告投放、基于位置信息的广告投放、基于社会网络的广告投放等新型应用模式对计算广告学发展的影响。

关键词：互联网广告行业计算广告学广告产业链投放形式 Web综合应用

来源：评论

学校读者我要写书评

暂无评论

一类积分不等式的机器判定

引用

中国科学：信息科学 2011年第1期41卷 48-65页

作者：杨路郁文生袁如意华东师范大学软件学院上海高可信计算重点实验室上海200062 中国科学院成都计算机应用研究所自动推理实验室成都610041 中国科学院自动化研究所综合信息系统研究中心北京100190

将一类积分不等式转化为Tarski模型外的齐次对称多项式不等式,该类齐次对称多项式的次数是给定的,变元个数可以是任意多个,并且多项式的系数是与变元个数相关的变系数.这些特点与杨路等人最近提出的几个公开问题密切相关,是比较有代表... 详细信息

将一类积分不等式转化为Tarski模型外的齐次对称多项式不等式,该类齐次对称多项式的次数是给定的,变元个数可以是任意多个,并且多项式的系数是与变元个数相关的变系数.这些特点与杨路等人最近提出的几个公开问题密切相关,是比较有代表性的一类齐次对称多项式.然后利用Timofte关于对称多项式不等式判定的降维方法,结合不等式证明软件BOTTEMA及差分代换方法,给出对应的一类Tarski模型外的齐次对称多项式不等式的机器判定算法,从而实现原积分不等式的机器判定.当给定的积分不等式及齐次对称多项式不等式不成立时,可给出具体不成立的数值反例.应用例子表明问题的广泛性及算法的有效性.

关键词：积分不等式对称多项式不等式 Timofte降维法差分代换机器判定不等式证明软件-BOTTEMA

来源：评论

学校读者我要写书评

暂无评论

基于环境的软件正确性形式化描述

基于环境的软件正确性形式化描述

引用

2011年第五届中国可信计算与信息安全学术会议(CTCIS2011)

作者：马艳芳张敏陈仪香淮北师范大学计算机科学与技术学院，安徽淮北 235000 华东师范大学软件学院，上海 200062 上海市高可信计算重点实验室，上海 200062

软件的运行依赖于环境，在考察软件正确性时需要考虑环境的因素。软件在开发和设计过程中，其正确性是一个逐渐改进的过程，也就是说，通过不断地修改，软件越来越接近于正确。为了刻画软件的这种动态正确性并考虑环境的因素，本文将以... 详细信息

软件的运行依赖于环境，在考察软件正确性时需要考虑环境的因素。软件在开发和设计过程中，其正确性是一个逐渐改进的过程，也就是说，通过不断地修改，软件越来越接近于正确。为了刻画软件的这种动态正确性并考虑环境的因素，本文将以三分之二互模拟为基础，利用网极限的观点，建立软件动态正确性的形式化描述。首先建立三分之二互模拟的无限演化理论，给出三分之二极限互模拟的定义。其次建立三分之二互模拟极限，这个极限在一定程度上反映软件规范是其实现的极限形式。最后证明三分之二互模拟极限与三分之二互模拟的相容性等性质。

关键词：运行环境软件规范极限形式进程演算

来源：评论

学校读者我要写书评

暂无评论

SHEPWM逆变器开关角度实解分类

SHEPWM逆变器开关角度实解分类

引用

2011 International Conference on Software Engineering and Multimedia Communication（SEMC）

作者：杨克虎宋力袁如意郁文生中国矿业大学(北京)机电与信息工程学院中国科学院自动化研究所综合信息中心华东师范大学上海高可信计算重点实验室

本文研究基于特定谐波消除脉宽调制技术(Selective Harmonic Eliminated PWM,SHEPWM)的逆变器开关角度的实解个数分类问题。利用变量代换将关于开关角度的非线性超越方程组转化为一个半代数系统,借助于半代数系统机器证明领域的最新成果... 详细信息

本文研究基于特定谐波消除脉宽调制技术(Selective Harmonic Eliminated PWM,SHEPWM)的逆变器开关角度的实解个数分类问题。利用变量代换将关于开关角度的非线性超越方程组转化为一个半代数系统,借助于半代数系统机器证明领域的最新成果,给出了一种对开关角度的实解个数进行解析分类的方法。并通过实例对N=3的三相双极型逆变器的开关角度进行了实解分类,验证了该方法的有效性,与已有的数值结果进行比较,该方法在理论上是完备的,能够得到精确的分类边界。

关键词：特定谐波消除逆变器脉宽调制半代数系统

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：