基于模糊神经网络的汽车类型自动识别分类系统

该文提出了一个基于模糊神经网络的汽车类型自动识别分类系统。在研制该系统的过程中，将模糊数学理论和神经网络相结合，建立了一个自适应的模糊逻辑与神经网络协作系统，成功地解决了在无专家经验的情况下，自动建立模糊隶属度函数和模糊识别规则的问题，具有较强的实用价值。     

基于归结的最大一般理论特化

提出一种基于归结的并有关于背景适应吸示例的一致特化理论,该理论给出了最大一般特化假设的归结构造方法,可将其作为一种蕴涵意义下的一般理论特化框架。基于该理论,进一步提出ｋ一般特化概念以解决特化的可计算性问题,并相应地给出特化算法。有关实验表明,该理论与算法能够正确并有效地进行一阶理论特化。     

闭环多体系统拓扑结构的动态搭建及其自动规则标号

基于将多体系统拓扑结构的形成看作是一个动态搭建过程，本文提出了一个能够由铰与物体之间关联矩阵自动选取切断铰并自动对物体和铰进行规则标号的算法．利用该算法，在建立系统动力学方程过程中可以采用铰坐标但无需人为选定切断铰，从而在很大程度上简化了输人工作有效地避免了很多人工错误．     

一种基于粗糙集的诊断型知识发现方法

知识获取是开发专家系统的瓶颈，传统的病害知识获取通常需要一个较长的过程．针对这一问题，本文给出了粗糙集理论和基于规则的作物病害知识之间的关系，即在油菜植病专家知识获取过程中的应用，建立了基于RHINOS 诊断模型的油菜病害的排除规则、包含规则和病害映像，阐述了可能性规则定义，并给出了基于规则描述的自动归纳推理方法，包括全搜索过程、后处理过程、统计测试的评估以及交叉验证和鞋带方法等．实验结果表明，粗糙集不仅是一个很好的知识获取的框架，而且能正确的归纳推理植物病害的规则．这对诊断型专家系统的开发可起到一个很好的辅助作用，在智能化农业信息系统中有着广泛的应用前景．     

基于配对方法的自动定理证明

ＰｅｔｅｒＢ．Ａｎｄｒｅｗｓ提出了自动定理证明的配对方法的理论和算法．本文针对该算法的缺点，给出了一个无需回溯的实现算法，并得到一个高阶逻辑的自动定理证明系统.     

基于MPEG-7框架的交互式图像层次化描述工具（IIHDT）的设计与实现

本文针对图像媒体类型，提出了一种基于MPEG-7框架的内容层次化描述模式，并在此基础上设计与实现了一个基于MPEG-7框架的交互式图像描述工具(IIHDT)。它除了能自动提取图像的元数据和通过人机交互对图像语义进行描述外，还能自动地提取图像的各种视觉特征，并形成描述。     

基于拍卖博弈的电子商务自动协商

为提高电子商务自动协商系统效率,本文以拍卖博弈理论为基础,提出并实现了一种基于拍卖博弈的自动协商Agent模型,并在此基础上实现了一个基于拍卖博弈的电子商务自动协商原型系统,应用于一个企业敏捷供应链管理系统中实现自动协商交易。     

知识发现的理论及其实现

本文提出知识的一种理论，该理论基于对人类知识发现认识过程的模拟，包括经验数据分类，各类数据的概念抽象，及概念间蕴涵关系的发现等步骤，文中介绍了实现这个理论的一个集成化学习系统ＫＤ３，以及它在自动建立专家系统知识库等方面的应用。     

COTN:基于契约的信任协商系统

基于改进的信任管理和协商技术，通过属性信任证实现多种类型的权限委托，设计并实现了一个基于契约的信任协商（COntract-based Trust Negotiation，COTN）系统．在该系统中，引入了基于契约的信任协商方法，既在契约确立过程中预先终止无法进行的协商请求，又在契约约定下的协商过程中研究了对信任证和访问控制策略中隐私信息的保护，以高效、可靠地自动建立信任关系．目前，COTN系统已在网格中间件平台CROWN中得以应用，并采用信任票据和策略缓冲机制提高系统运行性能．通过相关实验表明该系统具有较好的稳定性和可用性．     

基于通信的MAS内多Agent自动协商

给出了一个通用的基于联合意图的多Agent系统内部Agent协商模型，详细分析了Agent间的异步通信机制以及基于语言行为学的Agent自动协商语义，并在该协商语义的基础上给出了MAS内部基于联合意图的Agent自动协商通信协议，最后利用通信顺序进程验证了该协议的安全性和活性．     

Constructive logics Part I: A tutorial on proof systems and typed λ-calculi

The purpose of this paper is to give an exposition of material dealing with constructive logics, typed λ-calculi, and linear logic. The emergence in the past ten years of a coherent field of research often named “logic and computation” has had two major (and related) effects: firstly, it has rocked vigorously the world of mathematical logic; secondly, it has created a new computer science discipline, which spans a range of subjects from what is traditionally called the theory of computation, to programming language design. Remarkably, this new body of work relies heavily on some “old” concepts found in mathematical logic, like natural deduction, sequent calculus, and λ-calculus (but often viewed in a different light), and also on some newer concepts. Thus, it may be quite a challenge to become initiated to this new body of work (but the situation is improving, and there are now some excellent texts on this subject matter). This paper attempts to provide a coherent and hopefully “gentle” initiation to this new body of work. We have attempted to cover the basic material on natural deduction, sequent calculus, and typed λ-calculus, but also to provide an introduction to Girard's linear logic, one of the most exciting developments in logic these past six years. The first part of these notes gives an exposition of the background material (with some exceptions, such as “contraction-free” systems for intuitionistic propositional logic and the Girard translation of classical logic into intuitionistic logic, which is new). The second part is devoted to more current topics such as linear logic, proof nets, the geometry of interaction, and unified systems of logic (LU).     

Sequent calculi and decidability for intuitionistic hybrid logic

In this paper we study the proof theory of the first constructive version of hybrid logic called Intuitionistic Hybrid Logic (IHL) in order to prove its decidability. In this perspective we propose a sequent-style natural deduction system and then the first sequent calculus for this logic. We prove its main properties like soundness, completeness and also the cut-elimination property. Finally we provide, from our calculus, the first decision procedure for IHL and then prove its decidability.     

Hyperformulae, Parallel Deductions and Intersection Types

We aim at investigating the intersection-type assignment system for lambda calculus, with the Curry-Howard approach. We devise a propositional logic, whose notable characteristic is the presence of the hyperformulae denoting parallel compositions of formulae. As such, this logic formalizes a novel notion of parallel deductions, while forming a simple generalization of the standard natural deduction framework.We prove that the logical calculus is isomorphic to the intersection type system, by mapping logical deductions into typed lambda terms, encoding those deductions, and conversely. In this context the intersection type constructor, which comes out to be a proof-theoretic operator, is now interpreted as a standard propositional connective.     

Phase Semantics and Petri Net Interpretation for Resource-Sensitive Strong Negation

Wansing’s extended intuitionistic linear logic with strong negation, called WILL, is regarded as a resource-conscious refinment of Nelson’s constructive logics with strong negation. In this paper, (1) the completeness theorem with respect to phase semantics is proved for WILL using a method that simultaneously derives the cut-elimination theorem, (2) a simple correspondence between the class of Petri nets with inhibitor arcs and a fragment of WILL is obtained using a Kripke semantics, (3) a cut-free sequent calculus for WILL, called twist calculus, is presented, (4) a strongly normalizable typed λ-calculus is obtained for a fragment of WILL, and (5) new applications of WILL in medical diagnosis and electric circuit theory are proposed. Strong negation in WILL is found to be expressible as a resource-conscious refutability, and is shown to correspond to inhibitor arcs in Petri net theory.     

谓词形式系统(A)UL-h∈[0.75,1]及其可靠性

对基于一级泛与运算的一阶谓词演算形式系统(A)UL-h∈[0.75,1]进行公理化.通过引入全称量词和存在量词,建立与命题形式系统(A)UL-h∈[0.75,1]相对应的一阶谓词形式系统V(A)UL-h∈[0.75,1]并证明该系统的可靠性定理及演绎定理.     

Dijkstra-Scholten predicate calculus: concepts and misconceptions

The paper focusses on the logical backgrounds of the Dijkstra-Scholten program development style for correct programs. For proving the correctness of a program (i.e. the fact that the program satisfies its specifications), one often uses a special form of predicate calculus in this style of programming. We call this the Dijkstra-Scholten (DS) predicate calculus, since [DS90] is the first place in which it is described. DS predicate calculus can be conceived of as a logically sound and complete manipulation technique for dealing with logical formulas which also contain programming variables. We relate DS predicate calculus to the classical logical formalism, by contrasting its syntax, derivation rules and semantics to the classical framework. We also comment on two abstractions of DS predicate calculus: the set-theoretical and the algebraic approach. In doing so, we give DS predicate calculus and its abstract variants a firm basis, on a par with the foundations of the well-known first order logic. Such a comparison of DS predicate calculus and classical logic has not yet been sufficiently elaborated before. We conclude our paper with a number of examples showing that the, up to now, unsatisfactory presentation of DS predicate calculus and some of its features (such as the square brackets notation) has led to errors and fallacies in the literature. Received: 22 May 1997 / 5 May 1998     

一个MC逻辑及其逻辑程序的语义

本文定义了一个多ｃｏｎｔｅｘｔ逻辑结构。ＭＣＯ在几个方面推广了传统的一阶逻辑：每个ｃｏｎｔｅｘｔ相关一个理论；Ｃｏｎｔｅｘｔ间存在ｏｕｔｅｒ关系；     

A system that looks for axioms

In this paper we shall describe a formal system which enables us to prove theorems within propositional calculus, logic of quantifiers and first order theories, including theorems containing programs. Its main feature relies on generating an additional set of assumptions needed to prove a considered formula. Thus we are able to consider expressions which can become theorems by looking for a special set of assumptions (axioms) and then adding it to the standard set of axioms. Using this system the correctness and equivalence of programs can be determined. In the end we present some experimental results.     

Expressive Completeness of Duration Calculus

This paper compares the expressive power of first-order monadic logic of order, a fundamental formalism in mathematical logic and the theory of computation, with that of the propositional version of duration calculus (PDC), a formalism for the specification of real-time systems. Our results show that the propositional duration calculus is expressively complete for first-order monadic logic of order. Our semantics for PDC conservatively extends the standard semantics to all positive (including infinite) length intervals. Hence, in view of the expressive completeness, liveness properties can be specified in PDC. This observation refutes a widely believed misconception that the duration calculus cannot specify liveness properties.