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

基于矩形区域剖分的不等式机器证明方法—以Zirakzadeh的一个几何不等式为例

系统科学与数学 2010年第11期30卷 1430-1458页

作者：曾振柄张景中华东师范大学上海高可信计算重点实验室上海200062 中国科学院成都计算机应用研究所自动推理实验室成都610041

1988年,张景中,陶懋颀用细致的人工估计,用BASIC语言程序在PB700微型计算机上证明了Zirakzadeh于1964年证明的一个几何不等式,其方法是把不等式涉及的变量所在之区域剖分为一系列充分小的矩形,在每个小矩形上用数值方法验证若干三角函... 详细信息

1988年,张景中,陶懋颀用细致的人工估计,用BASIC语言程序在PB700微型计算机上证明了Zirakzadeh于1964年证明的一个几何不等式,其方法是把不等式涉及的变量所在之区域剖分为一系列充分小的矩形,在每个小矩形上用数值方法验证若干三角函数不等式的正确性.这个工作后来没有发表,将Zirskzadeh不等式转化为一个有3个变元的根式不等式,形如m_1^(/2)+m_2^(/2)+m_3^(/2)≥3m_4^(/2),其变量所在区域为一由6个线性不等式限制形成的多面体P(有14个顶点,21个棱和9个面),先用幂级数展开方法证明讨论的根式不等式在小长方体邻域[-0.1,0.1]~3C P成立,次将这个邻域以外的集合分割成有限多个边长不小于1/1280的小长方体或多面体,在每个小凸体上通过计算函数在顶点的取值和函数偏导数范围证明根式不等式的正确性.文章给出的验证数引理,可根据连续可微函数在长方体或一般凸多面体V的顶点的值,及函数偏导数的绝对值在集合V的上界,证明函数在V上的正定性.文章给出计算多项式在三维空间凸多面体上的最大值和最小值,以及估计根式函数的验证数的机械化方法.

关键词：数学机械化机器证明 Zirakzadeh不等式矩形剖分误差分析

来源：评论

学校读者我要写书评

暂无评论

命题逻辑系统中理论的真度概念及其应用

引用

陕西师范大学学报（自然科学版） 2009年第5期37卷 1-6页

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

首次在命题逻辑系统中引入理论的真度概念,将公式的真度推广为公式集的真度,从而简化了发散度的概念;进一步得出:当理论Γ相容时,理论的真度与相容度之间的关系为η(Γ)=(1+τ(Γ))/2;在命题逻辑系统C2中,将理论Γ1和Γ2分为六类,分别... 详细信息

首次在命题逻辑系统中引入理论的真度概念,将公式的真度推广为公式集的真度,从而简化了发散度的概念;进一步得出:当理论Γ相容时,理论的真度与相容度之间的关系为η(Γ)=(1+τ(Γ))/2;在命题逻辑系统C2中,将理论Γ1和Γ2分为六类,分别讨论了各类中理论Γ1、Γ2与Γ1∪Γ2的真度之间的关系.

关键词：理论的真度相容度发散度有限可数

来源：评论

学校读者我要写书评

暂无评论

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

引用

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

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

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

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

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

来源：评论

学校读者我要写书评

暂无评论

n值逻辑系统L_n~*中广义重言式的计量化研究

引用

陕西师范大学学报（自然科学版） 2009年第2期37卷 1-5,12页

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

基于均匀概率空间的无穷乘积,通过考虑使某一公式的赋值不小于(或大于)ζ(ζ∈[0,1])的那些赋值映射之集在总赋值集合中所占的份额,在n值R0-命题逻辑系统L*n中引入公式的ζ-真度及ζ+-真度概念,从而将重言式的概念进行双重程度化;提出了... 详细信息

基于均匀概率空间的无穷乘积,通过考虑使某一公式的赋值不小于(或大于)ζ(ζ∈[0,1])的那些赋值映射之集在总赋值集合中所占的份额,在n值R0-命题逻辑系统L*n中引入公式的ζ-真度及ζ+-真度概念,从而将重言式的概念进行双重程度化;提出了σ-(ζ-重言式)和σ-(ζ+-重言式)理论;研究了ζ-真度(ζ+-真度)与广义重言式及程度化的广义重言式之间的关系,给出了广义真度推理规则.

关键词：广义重言式 ζ-真度 σ-(ζ-重言式) 广义真度推理规则

来源：评论

学校读者我要写书评

暂无评论

BFSQ:处理空间成员查询的方法

引用

计算机科学与探索 2010年第8期4卷 692-699页

作者：张一桢金澈清胡颢继周傲英华东师范大学软件学院上海市高可信计算重点实验室上海200062

随着普适计算技术、定位技术、移动通讯技术的进步,移动对象数据管理技术在诸多领域中得到广泛应用。在移动对象数据管理领域中,隐私保护是一个不可忽视的问题。用户不仅期望获取高质量的服务,同时也期望能够尽量保护自身的隐私信息。... 详细信息

随着普适计算技术、定位技术、移动通讯技术的进步,移动对象数据管理技术在诸多领域中得到广泛应用。在移动对象数据管理领域中,隐私保护是一个不可忽视的问题。用户不仅期望获取高质量的服务,同时也期望能够尽量保护自身的隐私信息。研究了空间成员查询,检验在空间某区域内是否存在移动对象。所提出的BFSQ(Bloom filter-based spatial query)方法的一大特点是能够较好地保护移动数据/用户查询的隐私,同时查询结果的质量也维持在一个较高的水平。实验结果表明了新方法的高效率和有效性。

关键词：移动数据成员查询布隆过滤器隐私保护

来源：评论

学校读者我要写书评

暂无评论

基于多面体包含的非线性混成系统可达性分析

引用

计算机应用 2013年第5期33卷 1289-1293页

作者：邹进林望罗勇曾振柄温州大学数学与信息科学学院浙江温州325035 华东师范大学上海市高可信计算重点实验室上海200062

针对一类非线性混成系统的可达性问题,提出了一种基于多面体包含的分析方法。首先介绍了混成系统及其可达性,讨论了如何应用多面体包含对多项式混成系统进行线性近似,并采用量词消去和非线性优化方法来构造相应的线性混成系统,然后运用... 详细信息

针对一类非线性混成系统的可达性问题,提出了一种基于多面体包含的分析方法。首先介绍了混成系统及其可达性,讨论了如何应用多面体包含对多项式混成系统进行线性近似,并采用量词消去和非线性优化方法来构造相应的线性混成系统,然后运用验证工具SpaceEx求得原非线性混成系统的过近似可达集,并应用于验证系统的安全性。

关键词：混成系统可达性分析安全性验证多面体包含线性近似

来源：评论

学校读者我要写书评

暂无评论

线性系统的同时镇定问题

引用

控制理论与应用 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↓△代数完备性扩张

来源：评论

学校读者我要写书评

暂无评论

公钥密码安全强度刻画概述

引用

密码学报 2023年第5期10卷 879-896页

作者：林申陈洁王陆平华东师范大学软件工程学院上海高可信计算重点实验室上海200062 苏州科技大学电子与信息工程学院苏州215009 江苏省电梯智能安全重点建设实验室常熟215500

安全强度是对密码方案安全性的量化指标,代表了攻破某密码方案所需的计算开销.公钥密码方案的安全强度与构建该方案所依赖的困难问题和具体的参数有关.随着后量子密码学的发展,原先单一的安全强度评估标准产生了变化和扩充.因此,系统性... 详细信息

安全强度是对密码方案安全性的量化指标,代表了攻破某密码方案所需的计算开销.公钥密码方案的安全强度与构建该方案所依赖的困难问题和具体的参数有关.随着后量子密码学的发展,原先单一的安全强度评估标准产生了变化和扩充.因此,系统性总结数论体系下的经典公钥密码和抗量子攻击的后量子公钥密码的安全强度具有重要意义.本文首先介绍了经典公钥密码和后量子公钥密码的安全强度定义.然后给出了一些经典公钥密码方案的安全强度和后量子公钥密码方案的安全强度级别.接着从常见密码方案的现实应用出发,介绍若干在商用安全服务中使用的公钥密码方案及其安全强度分析.最后,给出本文的总结,并根据目前公钥密码安全性研究和应用的不足,对未来的研究和应用提出了展望.

关键词：安全强度经典公钥密码后量子公钥密码商用密码

来源：评论

学校读者我要写书评

暂无评论

偏差最小的四心圆近似椭圆作图法

引用

图学学报 2013年第1期34卷 9-16页

作者：曾振柄陈良育李志斌陈光喜华东师范大学软件学院上海200062 上海市高可信计算重点实验室上海200062 华东师范大学计算机科学技术学院上海200062 桂林电子工业学院计算科学与数学系广西桂林541004

以曲线的等距线距离为度量,得到近似椭圆与精确椭圆的偏差估计,并给出了偏差与半轴长的显示表达式。通过符号计算和回归分析,提出一种偏差最小的四心圆近似椭圆作图法。新方法易于通过尺规作图实现,可用于编制数控机床中加工椭圆零件的... 详细信息

以曲线的等距线距离为度量,得到近似椭圆与精确椭圆的偏差估计,并给出了偏差与半轴长的显示表达式。通过符号计算和回归分析,提出一种偏差最小的四心圆近似椭圆作图法。新方法易于通过尺规作图实现,可用于编制数控机床中加工椭圆零件的插补程序。

关键词：四心圆作图法偏差分析椭圆等距线

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：