摘要:本文提出了基于演绎和知识相结合的通过构造性证明综合程序的方法,进而讨论了不确定型逻辑程序的综合和自动综合的有关问题。用append程序的综合展示了这些方法。

摘要:随着正文数据应用的迅速增长,对正文数据检索方法的研究已成为数据库领域中令人感兴趣的课题之一。本文结合我国办公环境的特点,提出一种新的按附加码方法组织字标 识文件的正文数据库检索方法。这种方法不仅没有一般标识文件方法特有的“误选”现象,不必对查找标识文件后得出的文献进行全文扫描,而且处理查询时只需对标识文件进行范围查找,因此,其查询效率在较大范围内可以与正文检索方法中效率最高的倒排文件方法相近,并同时保持其它正文检索方法不具有的适应动态信息检索环境的优点。

摘要:在本文中,我们引进了算子模糊逻辑中的λ-蕴涵和λ-强蕴涵的概念,λ-逻辑结果和λ-弱逻辑结果的概念。证明了两子句的的λ-归结式是这两个子句的λ-逻辑结果,从而完成了λ-归结的完备性定理的证明。

摘要:本文介绍一种支持软件理解和复用的程序设计方法,以及实现该方法的实验性系统URS—1。

摘要:SBMTP(Simulate Boyer-Moore Theorem Prover)系统是在IBM-PC-386微机上用GCLISP语言实现的一个定理证明系统。该系统采用的思想方法和理论基础是Boyer-Moore的计算逻辑理论. SBMTP主要由三部分组成:知识库管理部分、定理证明部分及中断恢复部分。 知识库管理部分包括一个基本知识库和一系列知识库构造工具。用户可根据具体问题 灵活地组织自己所需要的知识库,定理证明部分采用启发式方法逐步推演,完成证明。中断恢复部分在证明产生中断的情况下提供了较强的恢复能力,提高了证明效率。

摘要:XYZ System is a CASE environment based on temporal logic and conforming to various ways of programming such as programming with HLL, hierarchical specification or production rules, sequential or concurrent, textual or graphical, etc. All these programming paradigms can be unified with a uniform framework of a temporal logic language. The system is designed with the idea to keep good balance between the theoretical rationalism and the engineering pragmatism. In this paper, this idea is illustrated from philosophical point of view.

摘要:本文讨论了软件自动化归纳途径的现状、症结和解决方法,介绍了归纳程序综合系统NDIPS的设计思想和实现技术,强调了系统中自动归纳程序的关键技术。