正向推理过程分析及UML建模

分析了正向推理专家系统中推理机的工作过程及其特征，使用UML建立了这一过程的use case模型、功能模型、交互模型。利用这些模型对正向推理专家系统的行为进行分析，提高系统的重用层次，改善专家系统的开发过程。     

A section is born: Studies in Automated Reasoning

A section is born: Studies in Automated Reasoning     

Validating the PSL/Sugar Semantics Using Automated Reasoning

The Accellera organisation selected Sugar, IBMs formal specification language, as the basis for a standard to drive assertion-based verification in the electronics industry. Sugar combines regular expressions, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) into a property language intended for both static verification (e.g. model checking) and dynamic verification (e.g. simulation). In 2003 Accellera decided to rename the evolving standard to Accellera Property Specification Language (or PSL for short). We motivate and describe a deep semantic embedding of PSL in the version of higher-order logic supported by the HOL 4 theorem-proving system. The main goal of this paper is to demonstrate that mechanised theorem proving can be a useful aid to the validation of the semantics of an industrial design language.     

Adding Action Refinement to a Finite Process Algebra

In this paper we present a Process Algebra for the specification of concurrent, communicating processes which incorporates operators for the refinement of actions by processes, in addition to the usual operators for communication, nondeterminism, internal actions, and restrictions, and study a suitable notion of semantic equivalence for it. We argue that action refinements should not, in some formal sense, interfere with the internal evolution of processes and their application to processes should consider the restriction operator as a "binder." We show that, under the above assumptions, the weak version of the refine equivalence introduced by Aceto and Hennessy ((1993) Inform. and Comput.103, 204-269) is preserved by action refinements and, moreover, is the largest such equivalence relation contained in weak bismulation equivalence. We also discuss an example showing that, contrary to what happens in Aceto and Hennessy ((1993) Inform. and Comput.103, 204-269), refine equivalence and timed equivalence are different notions of equivalence over the language considered in this paper.     

Process and Policy: Resource-Bounded NonDemonstrative Reasoning

This paper investigates the appropriateness of formal dialectics as a basis for nonmonotonic reasoning and defeasible reasoning that takes computational limits seriously. Rules that can come into conflict should be regarded as policies, which are inputs to deliberative processes. Dialectical protocols are appropriate for such deliberations when resources are bounded and search is serial.
AI, it is claimed here, is now perfectly positioned to correct many misconceptions about reasoning that have resulted from mathematical logic's enormous success in this century: among them, (1) that all reasons are demonstrative, (2) that rational belief is constrained, not constructed, and (3) that process and disputation are not essential to reasoning. AI mainly provides new impetus to formalize the alternative (but older) conception of reasoning, and AI provides mechanisms with which to create compelling formalism that describes the control of processes.
The technical contributions here are: the partial justification of dialectic based on controlling search; the observation that nonmonotonic reasoning can be subsumed under certain kinds of dialectics; the portrayal of inference in knowledge bases as policy reasoning; the review of logics of dialogue and proposed extensions; and the preformal and initial formal discussion of aspects and variations of dialectical systems with nondemonstrative reasons.     

Automated Reasoning and Equation Solving with the Characteristic Set Method

A brief introduction to the characteristic set method is given for solving algebraic equation systems and then the method is extended to algebraic difference systems. The method can be used to decompose the zero set for a difference polynomial set in general form to the union of difference polynomial sets in triangular form. Based on the characteristic set method, a decision procedure for the first order theory over an algebraically closed field and a procedure to prove certain difference identities are proposed.     

嵌入式系统同步进程的竞态条件分析与推理学习方法

针对嵌入式系统同步进程的竞态条件问题,提出了一个竞态条件分析与推理模型,包括竞态依赖集、竞态协作图和竞态条件数组三要素。其中,模型分析并推理嵌入式系统中具有竞态关系的进程,生成竞态依赖集,定义竞态协作图来描述同步进程竞态条件关系,设计竞态条件数组来存储进程竞态逻辑推理关系以便进一步学习分析。该分析与推理学习方法提高了分析效率,具有一定的实用价值。     

Towards Automated Case Knowledge Discovery in the M 2 Case-Based Reasoning System

In this paper we present the M ² Case-Based Reasoning (CBR) system. The M ² system addresses a number of issues that present methodologies for CBR systems have shied away from. We discuss techniques for removing the knowledge acquisition bottleneck when acquiring case knowledge. Here, case knowledge refers to the complementary knowledge structures, cases (more specific in nature) and adaptation rules (more general). We address the use of negative cases for updating the case knowledge as well as for refining the similarity measures. In particular we discuss in detail, showing experimental results, the use of Data Mining within the M ² system to build the case base from a database containing operational data, and discover adaptation rules. A methodology to monitor the competence of the CBR system and to utilize negative cases for updating the CBR system to enhance its competence is also discussed. The M ² CBR system also employs Rough Set and Fuzzy Set theories to further enhance its capabilities within real-world applications as well as providing a richer and truer model of human reasoning.     

Application of the Resources Model to the Supervision of an Automated Process

The present study was designed to ascertain how far flagging up potential errors can improve the automatic interpretation of technical documents. We used the resources model to analyze the supervised retro-conversion of architectural floor plans from the perspective of distributed cognition. Results showed that automated assistance helps users to correct errors spotted by the system and saves time. Surprisingly, they also showed that flagging up possible errors may make users less effective in identifying and correcting errors that go unnoticed by the system. Responses to a questionnaire probing the participants’ confidence in the system suggested that they were so trusting that they lowered their vigilance in those areas that had not been signaled by the system, leading to the identification of fewer errors there. Thus, although the participants’ confidence in the automated assistance system led to improved performances in those areas it highlighted, it also meant that areas to which the system did not draw attention were less thoroughly checked.     

案例推理及迭代学习在层流冷却控制中的应用

现有的卷取温度预报补偿模型和带钢批次间补偿模型中,由于案例推理(Case-based reasoning, CBR)系统中检索特征权重系数采用人工凑试的方法,难以获得满意的补偿作用,且由于缺乏迭代学习的初始工况条件的匹配算法,难以进行准确匹配和有效迭代.因此,本文针对这两个问题, 提出了基于神经网络技术的案例推理系统检索特征权重系数自动学习算法及迭代学习技术初始工况匹配算法,改进了卷取温度预报补偿模 型和带钢批次间补偿模型,并采用国内某大型钢厂的现场实际数据进行实验研究.实验结果表明,与原有方法相比,带钢卷取温度的控制偏差减小了1.63℃,卷取温度精度控制在±10℃以内的命中率提高了14.5%.     

表示和处理缺省知识的多维模糊推理方法及算法

本文采用MAX－○复合运算,在基于模糊关系Rb的多维模糊推理Sugeno-Takagi的推理框架中,利用可能性量化语句,从理论上提出了一种表示和处理和缺省知识的多维模糊推理方法,从而提高模糊推理表示和处理知识的能力。在此理论基础上,依据J.F.Baldwin真值限定的概念,提出了一种表示和处理缺省知识的多媒模糊真值推理算法。     

一个基于实例推理的软件过程知识复用方法

过程资产库的建立和基于过程资产的项目过程定义是一个组织的软件能力成熟度达到已定义级的关键标志,传统的过程资产库中存储的过程往往是通过文字描述和使用者判断其适用性,用于项目过程的建立。本文提出了一种基于实例推理(CBR)的过程知识复用方法,通过过程特征的刻画和实例相似度计算,实现过程实例的提取和复用。实践证明,该方法有助于提高过程知识复用的准确度和自动化程度,为软件过程改进中的过程建立提供有效手段。     

Application of Quantile Graphs to the Automated Analysis of EEG Signals

Neural Processing Letters - Epilepsy is classified as a chronic neurological disorder of the brain and affects approximately 2% of the world population. This disorder leads to a reduction in...