约束逻辑程序部分演绎过程的研究

约束逻辑程序的部分演绎是一个新兴的研究领域。本文提出了一个新的基于程序变换的ＣＬＰ部分演绎的过程。该过程以程序－目标为输入，经过一系列程序变换后终止，输出结果程序－目标对。该过程保证结果程序－目标对和输入程序－目标对计算等价，并且程序Ｐｎ解目标Ｑｎ比程序Ｐ０解目标Ｑ０效率更高。本文提出的方法语给出了一个ＣＬＰ程序部分演绎的运行这例。     

基于规则与基于实例的集成推理研究

基于实例推理（ＣＢＲ）与基于规则推理（ＲＢＲ）在许多决策支持系统中已得到了广泛的应用。如何有效地提高那些既含有演绎信息又含有类比信息的问题求解效率亦是专家系统开发者的研究课题之一。本文分析了ＣＢＲ和ＲＢＲ的优缺点，回顾了这两种推理方式的工作原理。针对ＲＢＲ与ＣＢＲ应用的局限性，本文提出了一种新的推理模式──ＲＢＲ与ＣＢＲ集成推理。这种模式既利用了ＣＢＲ的长处又利用了ＲＢＲ的优点，力图提高对含有不完整领域知识的问题的推理效率。     

利用CRC—32检测程序的完整性

本文提出了一种利用循环冗余校验和（ＣＲＣ）对程序的完整性进行校验的方法，给出了计算ＣＲＣ－３２的Ｃ语言算法程序，给软件开发者进行程序完整性检测提供了一种思路。     

规则推理和案例推理的集成研究

基于规则的推理（ＲＢＲ）和基于案例的推理（ＣＢＲ）是知识或两类实用有效的推理方式，文中提出了一种ＲＢＲ与ＣＢＲ相互集成的方法，为消除ＣＢＲ和ＲＢＲ结果之间的冲突，引入了逆案例，隐含规则和相似性度量等概念，以此提高了系统求解问题的效率，增强了系统对不良结构问题的适应性。     

Windows95和NT下的网络游戏开发(下)

其中所有的参数都取自ＥｎｕｍＳｅｓ－ｓｉｏｎｓ,系统每收到一个回复的消息便调用一次ＥｎｕｍＳｅｓｓｉｏｎ,并在结构ＬＰＤＰＳＥ－ＳＳＩＯＮＤＥＳＣ中添入适当的值。以下是ＥｎｕｍＳｅｓｓｉｏｎｓＣａｌｌｂａｃｋ的程序实例。ＢＯＯＬＦＡＲＰＡＳＣＡＬＥｎｕｍｓｅｓｓｉｏｎ（ＬＰＤＰＳＥＳＳＩＯＮＤＥＳＣｌｐＤＰＧａｍｅＤｅｓｃ,ＬＰＶＯＩＤｌｐＣｏｎｔｅｘｔ,ＬＰＤＷＯＲＤｌｐｄｗＴｉｍｅｏｕｔ,ＤＷＯＲＤｄｗＦｌａｇｓ）｛ＬＯＮＧｉｌｎｄｅｘ：ＨＷＮＤｈｗｎｄ＝（ＨＷＮＤ）ｌｐＣｏｎ－ｔｅｘｔ;／…     

含能材料化学合成专家系统ESCS的设计方法

本文为寻求合成某种物质的化学反应途径及步骤，设计出化学合成专家系统ＥＳＣＳ。本文包括如下部分：（１）化学反应式的知识表示与化学合成树的构造；（２）路段演绎规则；（３）在寻找合成途径中的应用；（４）路径优劣评价方法；（５）计算实例。     

防止DOS批处理被中断的TSR以及在局域网中的应用

本文介绍了用汇编语言设计的三个小程序，其中主程序是一个ＴＳＲ（终止并驻留）程序，用于彻底取消Ｃｔｒｌ＋Ｂｒｅａｋ和Ｃｔｒｌ＋Ｃ键盘中断，以防止一个ＤＯＳ批处理程序中途被中断退出，以增强批处理程序的安全性。     

基于FORM的CGI程序的设计与应用

本文介绍了基于ＦＯＲＭ的ＣＧＩ程序的实现方法，它通过ＨＴＭＬ（ｈｙｐｅｒＴｅｘｔＭａｒｋｕｐＬａｎｇｕａｇｅ）超文本标记语言的数据集表ＦＯＲＭ接收用户的数据并将这些数据提交给服务器，服务器再将其传递给ＣＧＩ程序，ＣＧＩ程序对数据进行处理，并处理后的信息返回给浏览器或进行其它处理。     

创建ORCAD软件的专用小汉字库

本文介绍了用于ＯＲＣＡＤ／ＳＤＴ软件的实用，灵活的专用小字库建立原理及过程，并用Ｔｕｒｂｏ Ｃ语言编制了由包含输入编码的汉字文本文件到汉字符号图形源文件（ＳＲＣ格式）的转换程序，给出了源程序和转换实例。     

CLP系统中推理机与约束求解器的协调技术

本文讨论了我们自行开发的ＢＰＵ－ＣＬＰ（Ｒ）系统中推理机与约束求解器的协调技术．协调主要发生在回溯机制中．本文描述的方法妥善地解决了在存储优化的情况下推理机与约束求解器的协调问题.     

启发式方法生成命题逻辑可读证明

探讨了自动生成命题逻辑系统R的可读证明.采用试探法和自然推理法分别从前推和后推模拟人类思维求证,试探法根据推理规则将待证公式反向分解,自然推理法从假设出发根据推理规则生成新的公式.两种方法都实现了相干命题逻辑系统R的可读证明,并结合实现了混合证明.试探法和自然推理法是生成可读证明的有效方法,前推和后推两种思维方法也适用于其他逻辑系统的自动证明.     

Automatic program verification I: A logical basis and its implementation

Summary Defining the semantics of programming languages by axioms and rules of inference yields a deduction system within which proofs may be given that programs satisfy specifications. The deduction system herein is shown to be consistent and also deduction complete with respect to Hoare's system. A subgoaler for the deduction system is described whose input is a significant subset of Pascal programs plus inductive assertions. The output is a set of verification conditions or lemmas to be proved. Several non-trivial arithmetic and sorting programs have been shown to satisfy specifications by using an interactive theorem prover to automatically generate proofs of the verification conditions. Additional components for a more powerful verification system are under construction.This research is supported by the Advanced Research Projects Agency under Contracts SD-183 and DAHC 15-72-C-0308, and by the National Aeronautics and Space Administration under Contract NSR 05-020-500.     

Rules and Strategies for Contextual Specialization of Constraint Logic Programs

We address the problem of specializing a constraint logic program w.r.t. a constrained atom which specifies the context of use of the program. We follow an approach based on transformation rules and strategies. We introduce a novel transformation rule, called contextual constraint replacement, to be combined with variants of the traditional unfolding and folding rules. We present a general Partial Evaluation Strategy for automating the application of these rules, and two additional strategies: the Context Propagation Strategy which is instrumental for the application of our contextual constraint replacement rule, and the Invariant Promotion Strategy for taking advantage of invariance properties of the computation. We show through some examples the power of our method and we compare it with existing methods for partial deduction of constraint logic programs based on extensions of Lloyd and Shepherdson's approach.     

Constrained partial deduction and the preservation of characteristic trees

Partial deduction strategies for logic programs often use an abstraction operator to guarantee the finiteness of the set of goals for which partial deductions are produced. Finding an abstraction operator which guarantees finiteness and does not lose relevant information is a difficult problem. In earlier work Gallagher and Bruynooghe proposed to base the abstraction operator oncharacteristic paths andtrees, which capture the structure of the generated incomplete SLDNF-tree for a given goal. In this paper we exhibit the advantages of characteristic trees over purely syntactical measures: if characteristic trees can be preserved upon generalisation, then we obtain an almost perfect abstraction operator, providing just enough polyvariance to avoid any loss of local specialisation. Unfortunately, the abstraction operators proposed in earlier work do not always preserve the characteristic trees upon generalisation. We show that this can lead to important specialisation losses as well as to non-termination of the partial deduction algorithm. Furthermore, this problem cannot be adequately solved in the ordinary partial deduction setting. We therefore extend the expressivity and precision of the Lloyd and Shepherdson partial deduction framework by integrating constraints. We provide formal correctness results for the so obtained generic framework ofconstrained partial deduction. Within this new framework we are, among others, able to overcome the above mentioned problems by introducing an alternative abstraction operator, based on so calledpruning constraints. We thus present a terminating partial deduction strategy which, for purely determinate unfolding rules, induces no loss of local specialisation due to the abstraction while ensuring correctness of the specialised programs. Michael Leuschel, Ph.D.: He currently works as a postdoctoral researcher at the Department of Computer Science of the Katholieke Universiteit Leuven. His present research focuses on program transformation and specialisation for declarative programming languages. Other research interests include abstract interpretation, optimised integrity checking and meta-programming. He received his degree (“Licence”) in Computer Science from the Université Libre de Bruxelles in 1990 and a Master of Artificial Intelligence from the Katholieke Universiteit Leuven in 1993, where he also received his Ph.D in 1997. Danny De Schreye, Ph.D: He is a professor at the Department of Computer Science of the Katholieke Universiteit Leuven and a senior research associate of the Belgian National Fund for Scientific Research. He obtained his Ph.D from K.U. Leuven in 1983, on the topic of operator algebras. His research interests are in the field of Logic Programming, and include program transformation and termination, knowledge representation and reasoning, and constraint programming.     

Constraint-based deductive model checking

We show that constraint logic programming (CLP) can serve as a conceptual basis and as a practical implementation platform for the model checking of infinite-state systems. CLP programs are logical formulas (built up from constraints) that have both a logical interpretation and an operational semantics. Our contributions are: (1) a translation of concurrent systems (imperative programs) into CLP programs with the same operational semantics; and (2) a deductive method for verifying safety and liveness properties of the systems which is based on the logical interpretation of the CLP programs produced by the translation. We have implemented the method in a CLP system and verified well-known examples of infinite-state programs over integers, using linear constraints here as opposed to Presburger arithmetic as in previous solutions. Published online: 18 July 2001     

Static and Dynamic Slicing of Constraint Logic Programs

Slicing is a program analysis technique originally developed for imperative languages. It facilitates understanding of data flow and debugging.This paper discusses slicing of Constraint Logic Programs. Constraint Logic Programming (CLP) is an emerging software technology with a growing number of applications. Data flow in constraint programs is not explicit, and for this reason the concepts of slice and the slicing techniques of imperative languages are not directly applicable.This paper formulates declarative notions of slice suitable for CLP. They provide a basis for defining slicing techniques (both dynamic and static) based on variable sharing. The techniques are further extended by using groundness information.A prototype dynamic slicer of CLP programs implementing the presented ideas is briefly described together with the results of some slicing experiments.