【摘 要】
：
In this paper, we provide a necessary infrastructure to define an abstract state exploration in the HOL theorem prover. Our infrastructure is based on a deep embedding of the Multiway Decision Graphs
【出 处】
：
Journal of Computer Science & Technology
论文部分内容阅读
In this paper, we provide a necessary infrastructure to define an abstract state exploration in the HOL theorem prover. Our infrastructure is based on a deep embedding of the Multiway Decision Graphs (MDGs) theory in HOL. MDGs generalize Reduced Ordere
其他文献
提出一种利用改进的3～(1/2)细分模式重建模型尖锐特征的算法。根据初始网格上标记的各种尖锐特征,通过修改3～(1/2)细分模式在不同特征处的几何规则,然后采用奇数次细分在尖锐边上插入两个新点、保持尖锐边不动,偶数次细分重新计算所有顶点坐标并连接两个新插入顶点的方法重建出初始网格上的各种尖锐特征。此外,还给出了算法的极限曲面在不同尖锐特征处的连续性分析。实验结果表明该算法具有较强的多分辨表达能力和
针对点到二维(2D)隐式曲线的正交投影问题,提出了一种稳定的几何迭代算法.分析隐式曲线在初始点处的曲率,将给定点向初始点处的切线或曲率圆作投影,并建立了追踪投影点的一阶和二阶泰勒迭代方法;在此基础上提出了基于曲率的步长控制策略;考虑到泰勒迭代方法产生的误差,进一步给出了基于梯度的迭代误差矫正方法.最后,给出了计算给定点到二维隐式曲线正交投影的完整算法.仿真结果表明,算法稳定、高效,收敛性良好.
借助于Packing问题的优化思想,提出了一种基于子模式类型的NAM优化策略.并比较了三角形子模式、矩形子模式以及三角形和矩形子模式混合的NAM表示方法,理论分析与实验结果均表明:基于子模式类型的NAM优化策略是行之有效的,对NAM的优化具有一定的指导意义.不断地逼近模式的最优化表示是NAM优化策略的最终目标,NAM优化问题在降低存储空间、提高传输速度、加快处理过程、模式匹配等方面具有理论参考意义
为了满足仿真系统中对仿真的实时性和视觉效果上的真实性要求,提出了一种改进的质点-弹簧模型,采用传统的质点-弹簧模型与虚拟弹簧共同表征图像的表面,利用Verlet数值积分更新图像变形期间的质点位置,使用双线性插值技术实时绘制出动态变形的效果.在OpenGL环境下对改进的3D质点-弹簧模型进行了仿真实验,实验结果表明所提模型能逼真地模拟出图像变形的效果.
针对传统主动轮廓模型在目标检测中存在的不足,对传统Snake算法进行了改进,用轮廓和目标间的频域距离来构造内力.分别研究了在单纯频域距离约束下和频域距离与图像力共同作用下Snake的变形行为.研究表明,在单纯频域距离约束下Snake能变形到目标、能量趋最小化,而在频域距离和图像力共同作用下Snake不能变形到目标.提出一种新的变参数Snake算法,该算法的变参数方式是让频域距离和图像力在Snake
介绍了奇异值的基本理论以及基于奇异值的图像分解方法,将奇异值分解方法应用于储粮害虫图像的压缩.为了与常规的图像压缩方法进行比较,在图像压缩比相同的情况下,通过分别计算jpg格式压缩和奇异值分解方法压缩的均方误差,计算结果表明,基于奇异值分解的图像压缩方法,误差小,效果良好,因此在储粮害虫的图像处理中具有很高的实用价值.
利用可见光图像和红外热图像进行图像融合是多模式人脸识别领域的一个新的研究方向.分别从特征级和决策级两个层次上研究了可见光图像和红外热图像的融合问题.在特征级上,引入遗传算法进行特征的优选,实现了两种图像的特征融合;在决策级上,提出利用Dempster-Shafer证据理论来实现决策的融合,并给出了具体的融合方案.分别采集了50人的红外热图像和可见光图像,每种各10张,共1000张图片进行了实验研究
A new method for constructing interpolating Loop subdivision surfaces is presented. The new method is an extension of the progressive interpolation technique for B-splines. Given a triangular mesh M,
We present some new methods for parameterizing the triangle mesh surface (TMS) which result from the Marching Cubes (MC) algorithm. The methods apply to surfaces of genus zero and the parameter domain
Polygonal models are popular representations of 3D objects. The use of polygonal models in computational applications often requires a model to properly bound a 3D solid. That is, the polygonal model