论文部分内容阅读
本文用类型一阶理论来定义逻辑程序，并通过引入Ｌａｋａｔｏｓ的基于证伪的发现方法论将原有的封闭型类型一阶理论改造为开放的类型一阶理论，在此基础上，建立了一个基于假说演算的逻辑自动程编程理论，并利用这一理论在Ｓｕｎ工作站上建立了一个自动设计Ｐｒｏｌｏｇ型程序的实验系统。
基于类型一阶理论的逻辑自动编程
【摘 要】
：
本文用类型一阶理论来定义逻辑程序，并通过引入Ｌａｋａｔｏｓ的基于证伪的发现方法论将原有的封闭型类型一阶理论改造为开放的类型一阶理论，在此基础上，建立了一个基于假说演算的逻辑自动程编
【机 构】
：
北京航空航天大学计算机科学与工程系
【出 处】
：
软件学报
【发表日期】
：
1994年11期
【基金项目】
：
国家高科技发展计划,国家自然科学基金
其他文献
本文首先引入了“变换型语言”的概念,给出了代表这种语言特征的机制:“变换模块”和“变换控制命令”的具体定义;举例说明了如何使用“变换模块”描述一个抽象数据类型的部
知识求精属知识获取的一个重要方面,旨在解决因知识不完全和噪音等因素引起的知识库正确性与有效性问题。本文通过知识库建造工具GKD—KBST中求精器KBRS实现方案的介绍,论述
本文证明了ＭｃＥｌｉｅｃｅ公钥体制中的公开钥矩阵实际上就是一个Ｇｏｐｐａ码生成矩阵，指出Ａｄａｍｓ和Ｍｅｉｊｅｒ对ＭｃＥｌｉｅｃｅ公钥体制安全性分析的不合理之处。本文的结果对Ｋｏｒｚｈｉｋ Ｔｕｒｋｉｎ攻击是一种理论上的支持并与一类基于纠错码的公钥体制
如何真正做到实践性、职业性、应用性，是应用型高等教育面临的一大重要课题。加强办学体制机制创新，推进合作办学、合作育人、合作就业、合作发展，增强办学活力显得尤为重要。本
主成分分析法是将分散在一组变量上的众多信息集中到少数几个综合指标（主成分）上，以便于描述数据集内部结构。本文运用主成分分析法，对新疆东方国际酒店及其竞争对手竞争力进行了
为了克服Ｌ．Ｆａｒｉｎａｓ ｄｅｌ Ｃｅｒｒｏ等人的命题模态归方法过多的符号冗余，我们增加了一条两个可能处子约束下公式的归结规则，称之为樗模态旭结方法，证明了标记模态归结的可靠性与完备性，这种新模态归结
天津市司法学校始建于1982年10月,是天津市唯一的一所全日制法律中专学校,隶属于天津市司法局。学校的培养目标主要是为天津市审判、检察、司法行政及社会各部门培养德、智、
本文提出了“面向对象的语义关联数据模型(CIM-OSA DM)”理论,在扼要介绍CIM-OSA DM的基础上,侧重于形式化地定义“对象”、“对象类”及类之间的“语义关联”,按照“对象”
英语词汇即多又乏味,不少学生深感生词记得快,忘得也快,常为此苦恼。在词汇教学中,我把心理学关于记忆的学说作为理论基础,根据记忆力的特点和规律,培养和发展学生的能力。记
本文给出了有界Petri网的可达标识图到网图的转换算法,对算法的正确性与复杂性分别进行了证明和估计,结果表明该算法是一个多项式算法,因而是有效的。