期刊文献+
共找到19篇文章
< 1 >
每页显示 20 50 100
SMT求解技术简述 被引量:12
1
作者 金继伟 马菲菲 张健 《计算机科学与探索》 CSCD 北大核心 2015年第7期769-780,共12页
SMT问题是在特定理论下判定一阶逻辑公式可满足性问题。它在很多领域,尤其是形式验证、程序分析、软件测试等领域,都有重要的应用。介绍了SMT问题的基本概念、相关定义以及目前的主流理论。近年来出现了很多提高SMT求解效率的技术,着重... SMT问题是在特定理论下判定一阶逻辑公式可满足性问题。它在很多领域,尤其是形式验证、程序分析、软件测试等领域,都有重要的应用。介绍了SMT问题的基本概念、相关定义以及目前的主流理论。近年来出现了很多提高SMT求解效率的技术,着重介绍并分析了这些技术,包括积极类算法、惰性算法及其优化技术等。介绍了目前的主流求解器和它们各自的特点,包括Z3、Yices、CVC3/CVC4等。对SMT求解技术的前景进行了展望,量词的处理、优化问题和解空间大小的计算等尤其值得关注。 展开更多
关键词 可满足性模理论(SMT) DPLL(T) 求解器
下载PDF
量化单一带标公式的消解
2
作者 金继伟 赵希顺 《中山大学学报(自然科学版)》 CAS CSCD 北大核心 2010年第1期20-23,共4页
在引入量化单一带标公式的概念后,给出其消解算法,并证明该消解算法是健全的和拒绝性完备的。因此该算法可用于对量化单一带标公式进行理论上的研究,同时也可用于在实际应用中解决这类公式的可满足性问题。最后,根据消解算法,得出一个... 在引入量化单一带标公式的概念后,给出其消解算法,并证明该消解算法是健全的和拒绝性完备的。因此该算法可用于对量化单一带标公式进行理论上的研究,同时也可用于在实际应用中解决这类公式的可满足性问题。最后,根据消解算法,得出一个可以在多项式时间内判定可满足性的量化单一带标公式的子类。 展开更多
关键词 量化单一带标公式 消解 可满足性 多项式时间可判定
下载PDF
量化带标公式的消解(英文)
3
作者 金继伟 赵希顺 《暨南大学学报(自然科学与医学版)》 CAS CSCD 北大核心 2009年第5期487-493,共7页
首先引入量化带标公式,然后研究了量化带标公式的消解并且证明其健全性和拒绝完备性.另外,还引入了二元消解并证明其针对正规量化带标公式(一个量化带标公式的子集)是健全的和拒绝完备的.最后证明如果正规量化带标公式的每一个子句如果... 首先引入量化带标公式,然后研究了量化带标公式的消解并且证明其健全性和拒绝完备性.另外,还引入了二元消解并证明其针对正规量化带标公式(一个量化带标公式的子集)是健全的和拒绝完备的.最后证明如果正规量化带标公式的每一个子句如果最多包含两个文字,则该公式的可满足性问题是易解的. 展开更多
关键词 消解 量化带标公式 正规 易解
下载PDF
内河航道交通信息管理系统应用软件的开发
4
作者 金继伟 刘向东 刘鹏 《水运工程》 北大核心 1996年第5期51-54,共4页
介绍内河航道交通量信息管理系统的基本原理、系统构成以及功能和特点,并对开发该系统的技术关键作了叙述。
关键词 内河航道 航道管理 交通量 信息管理系统
下载PDF
梳理棉毛纤维的锯齿带料感应器设计
5
作者 许滨 宋韶 金继伟 《工业加热》 CAS 2000年第6期49-50,共2页
主要介绍梳理棉毛纤维的锯齿带料感应器的设计 ,应用聚磁技术解决锯齿齿部加热均匀问题。
关键词 感应加热 感应器 锯齿带料 梳理棉毛纤维 设计
下载PDF
下穿既有铁路大跨度架空顶进箱涵的设计与施工关键技术 被引量:19
6
作者 金继伟 《郑州大学学报(工学版)》 CAS 北大核心 2012年第3期28-32,共5页
高速公路穿越既有铁路时,对于上覆填土较低大跨度斜交顶推箱涵的设计和施工始终是一个难点.结合洛三高速公路改扩建工程渑陈立交桥的工程,根据其上覆填土较低的特点,采用了架空顶进的方案.该方案针对铁道线路架空安全可靠性要求高、施... 高速公路穿越既有铁路时,对于上覆填土较低大跨度斜交顶推箱涵的设计和施工始终是一个难点.结合洛三高速公路改扩建工程渑陈立交桥的工程,根据其上覆填土较低的特点,采用了架空顶进的方案.该方案针对铁道线路架空安全可靠性要求高、施工过程中不间断铁路行车等特点进行了设计,系统地对线路加固方案中的便梁支墩挖孔桩的验算、顶进设计中的顶力计算、顶进设备、钢轨桩后背设计、施工时的施工条件、顶进作业工作顺序、施工注意事项等进行了详细阐述,解决了下穿既有铁路大跨度架空顶进箱涵的设计及施工关键技术,为同类工程提供了理论基础和工程实例,为解决上覆填土低的大跨度顶推箱涵提供了重要的技术支撑. 展开更多
关键词 下穿既有铁路 架空顶进 设计 施工技术
下载PDF
高速公路钢波纹管涵的研究及应用 被引量:8
7
作者 金继伟 《河南科学》 2012年第5期630-634,共5页
实践和研究均证明利用钢波纹管结构修筑涵洞更具有优势,也更具有广阔的应用前景.总结了河南省波纹管涵应用所取得的一些设计经验,并参考了国外一些先进的设计方法,对波纹管涵设计当中参数的确定、基础的处理及防腐处理、施工方法等关键... 实践和研究均证明利用钢波纹管结构修筑涵洞更具有优势,也更具有广阔的应用前景.总结了河南省波纹管涵应用所取得的一些设计经验,并参考了国外一些先进的设计方法,对波纹管涵设计当中参数的确定、基础的处理及防腐处理、施工方法等关键技术进行了全面、系统的论述,对波纹管涵的设计和施工具有一定的指导意义,这将对波纹管涵的推广应用起到了推动作用. 展开更多
关键词 高速公路 钢波纹管涵 设计 施工
下载PDF
桥台加固中预应力对拉锚杆技术的设计和应用研究 被引量:1
8
作者 金继伟 《河南科学》 2012年第7期938-941,共4页
预应力对拉锚杆技术在桥台加固中具有较大的优势,具有广阔的应用前景.结合张家庄公公分离式立交桥工程,从预应力对拉锚杆在桥台加固中的优点、锚杆的设计、钢筋混凝土网格梁的设计及施工要点等关键技术进行了全面地论述,系统地探讨在桥... 预应力对拉锚杆技术在桥台加固中具有较大的优势,具有广阔的应用前景.结合张家庄公公分离式立交桥工程,从预应力对拉锚杆在桥台加固中的优点、锚杆的设计、钢筋混凝土网格梁的设计及施工要点等关键技术进行了全面地论述,系统地探讨在桥台加固中预应力对拉锚杆的设计及应用. 展开更多
关键词 桥台侧墙 预应力对拉锚杆 设计 施工方案
下载PDF
浙江省航道地理信息系统概述 被引量:3
9
作者 金继伟 《交通科技》 2000年第3期16-18,共3页
结合浙江省航道管理计算机应用软件开发工作 ,介绍浙江省航道图文信息管理系统( CGW97)的功能、特点、运行环境 ,并就 CGW97的图形分层技术。
关键词 航道地理信息系统 CGW97 图形分层 数据共享
下载PDF
平原区高速公路通道排水系统研究及应用 被引量:3
10
作者 金继伟 《交通标准化》 2012年第9期89-92,共4页
针对平原区高速公路通道排水进行系统研究,从积水的原因、设计原则、计算方法等方面进行总结,针对不同积水条件系统地提出一系列的排水方案,对从根本上解决通道排水问题,降低平原区高速公路路堤高度提供了重要的技术支撑。
关键词 高速公路 通道 排水
下载PDF
高速公路改扩建工程中原有天桥利用的关键技术研究 被引量:1
11
作者 金继伟 白洪扬 《中外建筑》 2010年第4期134-136,共3页
本文结合工程实践对高速公路改扩建工程中原有天桥利用的关键技术问题进行了研究探讨,可供同类工程参考。
关键词 高速公路 改扩建工程 天桥 利用 拆除 保通
下载PDF
柴油机修理后的补充调整
12
作者 金继伟 郑殿斌 《农村实用科技信息》 2008年第6期51-51,共1页
经过修理后的柴油机.工况常达不到最佳指标,其主要表现为动力性能差、耗油量大、振动大、怠速不稳、高速排烟、怠速敲缸、加速不良、启动困难及容易过热等。出现这些情况的原因,一般是在柴油机的修理过程中,缺乏严格的检查制度和科... 经过修理后的柴油机.工况常达不到最佳指标,其主要表现为动力性能差、耗油量大、振动大、怠速不稳、高速排烟、怠速敲缸、加速不良、启动困难及容易过热等。出现这些情况的原因,一般是在柴油机的修理过程中,缺乏严格的检查制度和科学态度,只凭经验办事.或受修理条件的限制.致使所修零部件质量低劣。因此,修后的柴油机需根据具体工况进行适当的补充调整. 展开更多
关键词 修理过程 柴油机 调整 怠速不稳 零部件质量 动力性能 加速不良 启动困难
下载PDF
波形钢腹板箱梁无背索部分斜拉桥弹性稳定分析 被引量:3
13
作者 李宏瑾 李秋生 +1 位作者 吴继峰 金继伟 《中外公路》 北大核心 2011年第5期123-126,共4页
新密市溱水路大桥设计在中国首次采用了波形钢腹板无背索部分斜拉桥结构。笔者介绍了弹性稳定计算理论、研究第一类稳定问题的工程意义、基于数值解的第一类稳定问题的有限元分析方法和3种方法的稳定安全系数表达式。采用Midas/Civil屈... 新密市溱水路大桥设计在中国首次采用了波形钢腹板无背索部分斜拉桥结构。笔者介绍了弹性稳定计算理论、研究第一类稳定问题的工程意义、基于数值解的第一类稳定问题的有限元分析方法和3种方法的稳定安全系数表达式。采用Midas/Civil屈曲分析模块,按照上述方法3计算得到波形钢腹板箱梁无背索部分斜拉桥结构整体最小稳定安全系数及临界荷载,并进行了多阶弹性稳定分析。分析结果表明该桥梁结构稳定安全系数较大,整体稳定性较好。 展开更多
关键词 无背索部分斜拉桥 波形钢腹板 溱水路大桥 数值仿真 弹性稳定分析
原文传递
变速器油温过高的危害及变速器过热的成因 被引量:1
14
作者 郑殿斌 金继伟 张志强 《农村实用科技信息》 2008年第6期52-52,共1页
自动变速器正常的工作油温为80—90℃,变速器工作温度过高,会造成油液过早氧化,特别是变速器的工作温度超过120~200℃时,油液中的抗氧化添加剂失效,油液氧化速度急剧加快。
关键词 自动变速器 油温过高 抗氧化添加剂 原因 过热 危害 工作油温 温度过高
下载PDF
波形钢腹板箱梁无背索部分斜拉桥局部应力分析 被引量:1
15
作者 李宏瑾 金继伟 《中外公路》 北大核心 2011年第6期160-163,共4页
新密市溱水路大桥为中国第一座波形钢腹板箱梁无背索部分斜拉桥。采用全桥结构数值仿真技术和组合有限元思想,在建立桥梁精细有限元整体计算模型基础上,将关键部位有限元网格细化,得到索塔锚固区、索梁锚固区、墩梁塔固结区域局部应力,... 新密市溱水路大桥为中国第一座波形钢腹板箱梁无背索部分斜拉桥。采用全桥结构数值仿真技术和组合有限元思想,在建立桥梁精细有限元整体计算模型基础上,将关键部位有限元网格细化,得到索塔锚固区、索梁锚固区、墩梁塔固结区域局部应力,对结构局部受力性能进行研究分析,为优化设计提供了依据,并总结局部关键部位设计经验,为今后设计提出建议。 展开更多
关键词 波形钢腹板 无背索 部分斜拉桥 局部应力分析 溱水路大桥 数值仿真
原文传递
高速公路上跨天桥的美观设计 被引量:1
16
作者 闫卫红 金继伟 岳建光 《交通标准化》 2004年第8期99-100,共2页
高速公路上跨天桥应造型优美,型式多样,并与实际地形、环境相结合,以“合理的造价,可行的施工,可靠的 质量”来实现美观与设计的完美结合。
关键词 高速公路 上跨天桥 设计
下载PDF
孔内深层超强夯法(SDDC)作用机理及其在公路工程中的应用 被引量:9
17
作者 金继伟 卢淑萍 王春江 《公路》 北大核心 2000年第9期27-31,共5页
概要论述孔内深层强夯法 (SDDC)作用机理和特点 ,并以工程实例介绍该技术在公路工程上的应用效果。
关键词 孔内深层超强夯 作用机理 效果检验 公路工程
原文传递
灰土挤密桩处理三灵高速公路湿陷性黄土地基及检验效果 被引量:2
18
作者 金继伟 卢淑萍 王春江 《公路》 北大核心 2001年第9期70-72,共3页
概述了灰土挤密桩工作原理 ,介绍了三灵高速公路灰土挤密桩设计与施工要求 。
关键词 高速公路 湿陷性黄土 灰土挤密桩 挤密影响区半径 检验效果 地基
原文传递
Integrating Standard Dependency Schemes in QCSP Solvers 被引量:1
19
作者 Ji-Wei Jin Fei-Fei Ma Jian Zhang 《Journal of Computer Science & Technology》 SCIE EI CSCD 2012年第1期37-41,共5页
Quantified constraint satisfaction problems (QCSPs) are an extension to constraint satisfaction problems (CSPs) with both universal quantifiers and existential quantifiers. In this paper we apply variable ordering... Quantified constraint satisfaction problems (QCSPs) are an extension to constraint satisfaction problems (CSPs) with both universal quantifiers and existential quantifiers. In this paper we apply variable ordering heuristics and integrate standard dependency schemes in QCSP solvers. The technique can help to decide the next variable to be assigned in QCSP solving. We also introduce a new factor into the variable ordering heuristics: a variable's dep is the number of variables depending on it. This factor represents the probability of getting more candidates for the next variable to be assigned. Experimental results show that variable ordering heuristics with standard dependency schemes and the new factor dep can improve the performance of QCSP solvers. 展开更多
关键词 quantified constraint satisfaction problem standard dependency scheme variable ordering heuristics
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部