量词消去

作品数：19被引量：9H指数：2
导出分析报告
相关领域：理学自动化与计算机技术更多>>
相关作者：沈复兴傅莺莺罗里波吴茂念沈云付更多>>
相关机构：北京师范大学北京航空航天大学贵州大学上海大学更多>>
相关期刊：《首都师范大学学报（自然科学版）》《北京工业大学学报》《计算机应用与软件》《宿州学院学报》更多>>
相关基金：国家自然科学基金浙江省自然科学基金国家重点实验室开放基金北京市教委面上项目更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于实时自动机的连续时段演算的验证被引量：2
《软件学报》2019年第7期1953-1965,共13页安杰 张苗苗 
国家自然科学基金(61472279)~~
时段演算是描述和推导嵌入式实时系统和混成系统性质的一种区间时态逻辑。扩展线性时段不变式是时段演算的重要子集。针对实时自动机,提出一种连续时间语义下扩展线性时段不变式的有界模型检验方法。该方法将扩展线性时段不变式的有界...
关键词：时段演算 扩展线性时段不变式 量词线性算术 量词消去 
量词可消去的线性序理论
《宿州学院学报》2017年第10期96-98,共3页杜芬芬 陈国龙 
安徽省高校自然科学研究重大项目(KJ2014ZD31)
量词消去法在模型论的证明中是应用很广的一种方法。本文主要讨论在语言L=<,{0}上的有首元但无末元的稠密线性序理论T和在语言L_0={<}上的无末元离散线性序理论T_0的量词可消去性,及其在扩充语言L_1=S,{<}下理论T0的量词消去性。
关键词：稠密 离散 线性序 量词消去 
LIUF理论量词公式的插值算法
《软件工程与应用》2015年第6期121-128,共8页李千卉 江建国 刘文秀 
量词公式的插值是LIUF理论中一个未解决的问题。针对如何消去量词、消去量词后如何求出公式的插值等问题,提出了一种基于无量词公式理论插值的新算法。首先利用斯科拉姆化消去存在量词,并通过引入新变量消去全称量词,使量词公式变为无...
关键词：理论插值 LIUF理论 量词消去 斯科拉姆化 
可量词消去的带根节点的树理论
《数学学报（中文版）》2015年第4期691-704,共14页傅莺莺 沈复兴 
国家自然科学基金(61304155;11401015;11101012);北京市高校创新人才项目(201306206);北京市教委面上项目(KM201510011001);北京工商大学青年教师科研启动基金(QNJJ2014-27)
讨论了带根节点r的有向树、无向树理论的量词消去性质,找到决定理论量词消去的三类特殊公式,并给出了在语言■_0={E,r}(E为有向边或无向边)及添加二元距离关系D_(n,n)
关键词：量词消去 有向树 无向树 
可量词消去的树形偏序理论的分类
《数学学报（中文版）》2014年第6期1171-1180,共10页傅莺莺 沈复兴 
国家自然科学基金资助项目(61304155;11101012;11401015);北京工商大学青年教师科研启动基金(QNJJ2014-27)
提出了偏序的全序片段、序模式的概念以刻画树形偏序的结构特征,以此为基础,讨论了有最小元0的树形偏序理论的量词消去性质,给出了在语言(?)_0={<,0}及其膨胀语言下可以量词消去的这类理论的完全分类。
关键词：偏序 量词消去 序模式 树结构 
一种基于可处理不等式约束的动态几何自动作图软件GeoDraw
《计算机应用与软件》2012年第9期41-44,65,共5页赵婷 
法国国家科研署和中国国家自然科学基金联合项目(ANR-09-BLAN-0371-01/60911130369);软件开发环境国家重点实验室开放课题项目(SKLSDE-2011KF-02)
针对目前大部分几何作图软件只能处理等式约束的不足,设计并实现一种基于可处理不等式约束的动态几何自动作图软件GeoDraw。该软件应用符号和数值混合计算,将构造式和生成式作图方法相结合,可以有效地生成含有不等式约束的动态几何图形...
关键词：动态几何图形 自动作图 不等式约束 符号和数值计算 生成式作图 三角分解 量词消去 
一类特殊的双向归纳环
《首都师范大学学报（自然科学版）》2011年第4期8-10,共3页马鑫 王来 
证明了在语言L={+,.,0,1}下,带有一阶可定义序关系的环理论扩充到具有量词消去时,其模型是双向归纳环,进而得出一类特殊的双向归纳模型.
关键词：双向归纳环 量词消去 双向归纳模型 
基于量词消去的Petri网不变式自动生成
《上海电力学院学报》2011年第1期75-78,86,共5页毕忠勤 
上海市优秀青年教师培养基金(SDL10010)
基于模板和量词消去建立了一个求解Petri网不变式的算法.引入一个带参模板作为Petri网的候选不变式,再根据不变式必须满足归纳断言初始条件和承接条件,将Petri网的自动生成问题转化为量词消去问题,并求解出带参模板中的参数得到原Petri...
关键词：PETRI网 不变式 量词消去 半代数变迁系统 
完全稠密二叉偏序理论的量词消去(Ⅰ)
《北京师范大学学报（自然科学版）》2008年第6期568-572,共5页陈磊 沈复兴 
北京师范大学青年教师基金资助项目
给出了完全稠密二叉偏序理论在语言L={≤,R}中的公理集,证明了在语言L={≤,R}中,该理论具有不可量词消去的性质.同时提出了该理论在L={≤,R,*}中的六类基本公式,通过考虑不同基本公式合取的量词消去情况,来证明完全稠密二叉偏序理论在语...
关键词：量词消去 完全稠密二叉偏序 基本公式 同类公式 
完全稠密二叉偏序理论可量词消去的新证明
《北京师范大学学报（自然科学版）》2008年第2期111-114,共4页傅莺莺 沈复兴 吴茂念 
国家自然科学基金资助项目(60310213)
利用理论的代数素模型和简单闭性质,给出了完全稠密二叉偏序理论可量词消去的新的简短的证明.
关键词：量词消去 完全稠密二叉偏序 代数素模型 简单闭性质 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部