清华大学出版社最新图书

《逻辑程序语言及其实现技术》 本书详细论述了逻辑程序设计语言的实现技术和面向逻辑程序设计语言的体系结构。其主要内容包括:逻辑程序理论基础,Prolog语言简介,WAN编译技术,WAM的扩充和优化,顺序推理机体系结构,逻辑程序并行处理方法和模型,抽象解释技术,并行逻辑程序设计语言及其实现技术、并行推理机体系结构等。     

逻辑推理理论的定量发展

本文在一阶谓词逻辑的基础上,为每个定性的Horn子句规则赋予一个蕴涵强度f,从而得到定量的f-Horn子句规则及其Herbrand解释.最后,我们成功地给出了f-Horn子句规则的模糊过程解释,并由此引入了模糊逻辑程序系统.     

Linux进程语义安全性检测的稳定模型

现有进程检测方法,检测的目标是系统调用的序列的排列关联,忽略了语义中潜在的异常。稳定模型是逻辑程序的语义模型,可以用以发现并修改逻辑程序的异常问题。该文以系统调用为基本检测点,采用逻辑程序描述进程的基本语义逻辑,用稳定模型表达进程的检测语义。系统定义进程的一系列安全语义规则,在进程执行中,计算安全语义规则与进程逻辑之间的稳定模型,得到安全语义的可计算性结论。论文最后,给出了一个Linux系统中的进程语义安全性检测的基本框架。     

基于J2EE分布式环境的再工程方法

给出基于J2EE分布式环境的遗留系统再工程框架。应用改进的层次聚类算法提取系统组件,能够方便地将代码取出以构建分布式系统。给出适用于J2EE 分布式环境的组件接口启发式规则和模块部署策略。实现企业遗留系统到J2EE分布式系统的再设计过程,验证该框架的强壮性、实用性和通用性。     

并行逻辑程序系统RAP/LOP-WAM中的并行调度策略和否定的并行实现

本文论述并行逻辑程序系统RAP/LOP-WAM中的并行调度策略和否定的实现。受限与/或并行执行逻辑程序模型RAP/LOP,采用改进的RAP技术开发与并行,即通过程序级和子句级的分析,动静相结合识别子句体中子目标间的数据相关性,开发独立目标的与并行,OR并行的开发受限于处理机个数,有效地控制了进程数和空间量的指数爆炸。RAP/LOP相应的抽象机称为RAP/LOP-WAM,它基于OR树林描述,扩展WAM支持受限与和或并行执行逻辑程序。本文这里首先描述RAP/LOP-WAM中的并行调度策略,分析评价了几种调度算法及它的实现方法。其次论述了否定的实现方法,最后提出了今后我们研究的方向。     

一种基于进程代数的安全协议验证消解算法

安全协议本质上是分布式并发程序,可以描述为多个子进程的并发合成系统.将安全协议对应的并发合成系统抽象为一组逻辑规则,能够对安全协议无穷会话的交叠运行进行验证.本文首先给出了将安全协议基于进程代数的形式描述转化成为一组逻辑规则的方法,并提出了基于逻辑规则分类的高效逻辑程序消解算法,对安全协议认证性和保密性进行验证.     

在函数式程序设计系统上进行逻辑程序设计

本文揭示逻辑程序设计语言与函数式程序设计(FP)语言之间的一种内在联系。文中工作表明,在FP系统上进行逻辑程序设计是可行的。用例子阐明了,在FP系统上如何进行Horn子句逻辑程序设计;并且指出了,在FP系统上进行逻辑程序设计的一般法则,这些法则如加以进一步细化并用FP语言编成翻译程序,则在FP系统上更可直接地进行Horn子句逻辑程序设计。     

一种基于逻辑程序的重复协商框架

本文从基于信念修改的角度提出了两个AGENT之间的一个重复协商框架.在这个框架中,一个逻辑程序被当作一个协商的AGENT,每一个AGENT(逻辑程序)选择自己的一个回答作为自己最初的协商需求.两个AGENT之间的协商过程就是两个逻辑程序之间相互更新的过程,这个过程是通过协商的每一方接受对方的部分(或,全部)需求和放弃自己部分协商需求来实现的.本文设计了协商双方必须遵守的一些协商规则,根据这些规则对这个协商框架进行了形式化描述,并给出了协商的终止条件.     

二维优化排样方法及实现技术

在工业应用领域中存在大量的二维下料问题,其中应用最多的是矩形件下料问题.矩形件下料问题的关键是寻找二维平面的优化布局.针对工业生产中实际存在的问题与约束条件,给出了新的规则设计理论和数据模型,利用覆盖率和有效覆盖率的概念来控制余料合并操作的执行,运用布局规则、组合规则和切割规则给出了一种新的启发式算法.实验分析和工业应用证明,该启发式算法可以有效地提高板材的整体利用率,极大地减少了板材损耗.     

基于逻辑程序的安全协议验证

安全协议本质上是分布式并发程序，可以自然地描述为多个子进程的并发合成系统．将安全协议对应的并发合成系统抽象为逻辑程序进行消解，能够对安全协议无穷多个会话的交叠运行进行验证．该文提出了安全协议逻辑程序中逻辑规则的一个分类方法，基于该分类方法提出了安全协议逻辑程序不动点的迭代计算方法．逻辑规则的分类优化了安全协议逻辑程序不动点的迭代计算和安全性质验证过程中的计算．由于安全协议逻辑程序不动点迭代计算过程不一定终止，文中提出了每进行k≥1步安全协议逻辑程序不动点迭代计算验证一次安全性质的验证策略．     

Specification and correctness proof of a WAM extension with abstract type constraints

We provide a mathematical specification of an extension of Warren's Abstract Machine (WAM) for executing Prolog to type-constraint logic programming and prove its correctness. Our aim is to provide a full specification and correctness proof of a concrete system, the PROTOS Abstract Machine (PAM), an extension of the WAM by polymorphic order-sorted unification as required by the logic programming language PROTOS-L.In this paper, while leaving the details of the PAM's type constraint representation and solving facilities to a sequel to this work, we keep the notion of types and dynamic type constraints abstract to allow applications to different constraint formalisms like Prolog III or CLP(R). This generality permits us to introduce modular extensions of Börger's and Rosenzweig's formal derivation of the WAM. Since the type constraint handling is orthogonal to the compilation of predicates and clauses, we start from type-constraint Prolog algebras with compiled AND/OR structure that are derived from Börger's and Rosenzweig's corresponding compiled standard Prolog algebras. The specification of the type-constraint WAM extension is then given by a sequence of evolving algebras, each representing a refinement level, and for each refinement step a correctness proof is given. Thus, we obtain the theorem that for every such abstract type-constraint logic programming system L, every compiler to the WAM extension with an abstract notion of types which satisfies the specified conditions, is correct.The first author was partially funded by the German Ministry for Research and Technology (BMFT) in the framework of the WISPRO Project (Grant 01 IW 206). He would also like to thank the Scientific Center of IBM Germany where the work reported here was started.     

A typed functional extension of logic programming

A logic language is suitable for specification if it is equipped with features for data abstraction and modularization. In this paper, an effective mechanism to incorporate function and type into logic programming is presented as the means to embed data abstraction mechanism into logic programming. This incorporation is essentially based on Horn clause logic with equality and a polymorphic type system that is an extension of Mycroft and O’Keefe’s system. This paper also presents an implementation based on Warren Abstract Machine (WAM) and shows the performance, along with a comparison with WAM.     

DWAM — A WAM model extension for disjunctive logic programming

Answering queries in disjunctive logic programming requires the use of ancestry-resolution. The resulting complication makes it difficult to implement a Prolog-type query answering procedure for disjunctive logic programs. However, SLO-resolution provides a mechanism which is similar to SLD-resolution and hence offers a solution to this problem. The Warren Abstract Machine has been a very effective model for implementing Prolog. In this paper, we extend the WAM model of Prolog and adapt it for DISLOG — a language for disjunctive logic programming. We describe the extensions and additional instructions needed to make WAM viable for modeling and executing DISLOG. The extension is made in such a way that the original architecture is not disturbed and a Prolog program will execute as efficiently as it does in the original WAM.This work was done while the author was at the University of Kentucky.     

Predicates and pixels

This paper explores the possibilities of programming with graphical representations of logic programs. Two example programs are given in the concurrent logic language FGDC but many languages based on rewrite rules would be suitable for the same treatment. A graphical syntax promises to make programming in suitable ultra high level languages easier and more intuitive.     

Refinement of a typed WAM extension by polymorphic order-sorted types

We refine the mathematical specification of a WAM extension to typeconstraint logic programming given in [BeB96]. We provide a full specification and correctness proof of the PROTOS Abstract Machine (PAM), an extension of the WAM by polymorphic order-sorted unification as required by the logic programming language PROTOS-L, by refining the abstract type constraints used in [BeB96] to the polymorphic order-sorted types of PROTOS-L. This allows us to develop a detailed and mathematically precise account of the PAM's compiled type constraint representation and solving facilities, and to extend the correctness theorem to compilation on the fully specified PAM.The first author was partially funded by the German Ministry for Research and Technology (BMFT) in the framework of the WISPRO Project (Grant 01 IW 206). He would also like to thank the Scientific Center of IBM Germany where the work reported here was started.     

The safety-bag expert system in the electronic railway interlocking system elektra

The real-time expert system “Safety-Bag” is an integral part of the electronic railway interlocking system ELEKTRA. The interlockinh system contains a logic channel, which processes commands, and a safety channel, which checks the commands according to safety rules. Commands which are only allowed under certain circumstances are carried out only if the instructions generated by processing the command in the logic channel are checked and committed by the safety channel. To minimize the possibility of common errors in both channels, different programming paradigms are used. The logic channel is implemented in a procedural programming language and the Safety-Bag is implemented in PAMELA, a rule-based expert system language suitable for real-time applications. The rule-oriented programming paradigm is very well suited to the Safety-Bag because the safety requirements themselves are represented by rules. The Safety-Bag runs on a standard ALCATEL process control computer.     

A parallel parsing system for natural language analysis

The paper presents a parallel parsing system for Definite Clause Grammars suitable for committed-choice parallel logic programming languages. Grammatical elements such as words and nonterminal symbols are defined as parallel processes. Parsing is done by the processcommunication. The advantage of the system is that all the grammar rules are compiled into the parallel logic programming language and the program has neither any side-effect nor duplicated computation.     

Towards a complete framework for parallel implementation of logic languages: the data parallel implementation of SEL

Although logic languages, due to their non-declarative nature, are widely proclaimed to be conducive in theory to parallel implementation, in fact there appears to be insufficient practical evidence to stimulate further developments in this field. The paper puts forward various complications which arise in assuming a solely process parallel approach as a possible explanation for this situation. As an alternative, data parallelism is posited as an underutilized forte of logic programming. The paper illustrates a data parallel implementation of a particular language called SEL which is based on sets. Thus, SEL (set equational language) is introduced as an example of logic language which lends itself to an efficient data parallel implementation. The strategy of this implementation assumes an abstract machine called SAM (set-oriented abstract machine) which is based on the WAM (Warren abstract machine). SAM serves as an intermediary between the SEL language and the target machine for the implementation, the Connection Machine. Finally, some preliminary benchmarks are presented.     

A lingua franca for concurrent logic programming

Two of the more important concurrent logic programming languages with nonflat guards are GHC and Parlog. They balance the requirements of having clean semantics and providing good control facilities rather differently, and their respective merits are compared and contrasted. Since concurrent logic programming would benefit from both, but neither language is able to express all the programs expressible in the other language, a lingua franca of these languages is defined and justified. A method is given for translating GHC and Parlog to and from it. The method preserves the arities and execution conditions of each clause. It enables a lingua franca implementation to support both languages transparently, and to provide a simple concurrent logic programming language suitable for programming in its own right     

An experimental logic based on the fundamental deduction principle

Experimental logic can be viewed as a branch of logic dealing with the actual construction of useful deductive systems and their application to various scientific disciplines. In this paper we describe an experimental deductive system called the SYMbolic EVALuator (i.e. SYMEVAL) which is based on a rather simple, yet startling principle about deduction, namely that deduction is fundamentally a process of replacing expressions by logically equivalent expressions. This principle applies both to logical and domain-dependent axioms and rules. Unlike more well-known logical inference systems which do not satisfy this principle, herein is described a system of logical axioms and rules called the SYMMETRIC LOGIC which is based on this principle. Evidence for this principle is given by proving theorems and performing deduction in the areas of set theory, logic programming, natural language analysis, program verification, automatic complexity analysis, and inductive reasoning.