位置：立项数据库 > 立项详情页
项重写系统等价性的形式自动证明
  • 项目名称：项重写系统等价性的形式自动证明
  • 项目类别：面上项目
  • 批准号：60273015
  • 申请代码：F020509
  • 项目来源：国家自然科学基金
  • 研究期限：2003-01-01-2005-12-01
  • 项目负责人：冯速
  • 负责人职称：副教授
  • 依托单位：北京师范大学
  • 批准年度：2002
中文摘要：

本项目以各种归纳法及申请者设计开发的项重写系统元计算模型“动态项重写计算”为主要工具，确立项重写系统等价性的形式自动证明方法，证明该方法的正确性。同时，实现该方法，确认其有效性，探讨其有效范围，本项目是对于程序正确性的自动证明及可证明语言的设计开发方面的创新的和指导性的基础研究，研究还将确立弱终止性的形式自动证明方法。

中文主题词： 等价性;递归领域;形式自动证明;项重写系统;动态项重写计算
结论摘要：

英文主题词equivalence;recursive domain;automated formal proving;term rewriting system;dynamic term rewriting calculus

成果综合统计
成果类型
数量
  • 期刊论文
  • 会议论文
  • 专利
  • 获奖
  • 著作
  • 13
  • 3
  • 0
  • 0
  • 10
期刊论文
一种改进的分水岭人脑MR图像分割方法
基于数据挖掘的蔬菜图片病害自动分类
一种新的中文文本分类算法
基于人工免疫网络的k-平均聚类算法的研究
免疫遗传算法在排课问题中的应用
中国象棋Alpha-Beta搜索算法的研究与改进
动态虚拟私有网络:一种新的VPN实现方案
汉语分词技术研究现状与应用展望
博弈树搜索算法概述
基于概念层次网络的小学应用题句类分析和知识提取
博弈树搜索算法在中国象棋中的应用
一些5次数环的具有Goldbach性质的扩环
有限可补格上的一阶格值逻辑几个性质
会议论文
Xin Jin, Anbang Xu, Rongfang Bie, and Ping Guo,
国内,口头,冯速,计算机专业教学中课程软件的运用
国际,口头,Feng Su,Xiong Feng,WEAKLY GROUND TERMINATION OF MUTUALLY RECURSIVE TRSs
著作
基于DTRC的形式自动证明平台及其在TRS弱终止性自动证明的应用,
冯速,高效重写型程序的设计,
别荣芳,关于整数环的无限n素元组归纳扩环的多样性,
谢华美,何其翱,郑宁,别荣芳*,基于ERDAS 二次开发的遥感图像同态滤波薄云去除算法的改进
Bie Rongfang, Inductive rings and systems of diophantine equations,
Jin Xin, Bie Rongfang*, Classification Analysis of SAGE Data Using Maximum Entropy Model,
冯速,项重写系统弱基终止性的归纳证明,
Bie Rongfang, IBi-inductive Rings and Systems of Diophantine Equations?,
刘萍,别荣芳,基于交易数据库的关联规则生成算法FAS及其应用,
冯速,项重写系统等价性的归纳证明,
相关项目
基于非光滑切换的Filippov微分包含系统分析与设计研究
期刊论文 9 会议论文 6
在网络系统中多指标平衡问题的理论与方法研究
期刊论文 36
总体最小二乘估计理论及其在测绘数据处理中的应用研究
期刊论文 40
量子计算模型相关问题的研究
期刊论文 8
冯速的项目