基于解释的学习

近几年来,在机器学习领域,人们对基于解释的学习方法产生了极大兴趣。本文首先通过一个例子说明该学习方法,然后作了一般描述,并把它与基于类似的学习进行了比较,最后详尽讨论了基于解释的学习中的两个重要方面:操作性和不完善域论。     

蛋白质相互作用研究中的计算方法综述

随着分子生物学的研究进入以蛋白质组学为标志的后基因组时代,蛋白质相互作用成为蛋白质组学研究的一个重要主题.因为计算方法代价低和周期短的特点,它被广泛地用来分析相互作用数据从而指导生物学家的实验设计.从蛋白质相互作用网络的构建到分析两个方面综述了蛋白质相互作用研究中的各种计算方法:介绍了通过机器学习方法预测、文本挖掘和评估相互作用的各种技术;特别详细地阐述了相互作用网络的重要参数和典型生物模型,并对运用图论方法分析和计算的各种算法进行了深入的剖析;最后,对蛋白质相互作用的计算研究进行了总结和展望.     

软件工程学:过去、现在与未来

<正> 一、软件工程据Haberman的观点,工程是指为推进目标实现而创造的实体与机制。那么软件工程就是为推进软件生产的目标而创造的实体与机制。对软件工程的研究也就围绕着这两个方面展开。软件工程中的实体是指构成软件的基本块,用来构造软件的工具与环境。对这些实体的研究,可与传统工程中“硬”科学相类比。作为一种生、产活动,就要有一定的工具。工具的好坏是衡量生产力水平的重要标准。在软件生产中,常用的工具有编辑器,语言分析器,解释器,调试器,标准打印程序等。也有辅助管理的软件,如数据字典,     

一门新的面向构件语言

作为软件体系结构的重要贡献之一，连接子显式地描述了构件之间的交互．本文认为连接子的重要性值得我们在程序设计语言中加以支持．提出了一门新的面向构件语言SAJ，把构件，端口，连接子等软件体系结构概念引入到SAJ中．连接子与构件在SAJ中都是一阶实体，使得软件体系结构在底层实现中更加显式化，而且能更好地支持构件和连接子的复用．给出了SAJ语言的语法、语义和类型系统，并说明其具有类型安全性．     

结构化证明搜索

本文在简介证明开发环境的元语言ＴＭＬ之后，提出两类结构化设施；模块化机制为元级程序设计提供模块化手段；抽象理论机制用来描述定理证明赖以进行的背景理论．联合使用模块机制和结构化理论描述，系统可自动实现结构化证明搜索．     

支持智能体的通讯原语库系统GKD－APS的设计与实现

ＧＫＤ－ＡＰＳ是我们基于面向智能体程序设计范例，设计并实现的一个支持智能体相关概念及智能体间消息通讯的Ｐｒｏｌｏｇ解释器。它同时引入了智能体、精神状态、知识、信念、承诺、能力及智能体间的消息通讯等概念，并提供了对这些概念的直接支持。ＣＫＤ－ＡＰＳ为实现多智能体间的知识通讯和合作运行，构造多智能体系统提供了基础，有效地支持了分布式知识系统的研究和开发。本文首先介绍了当前国际上关于智能体及面向智能体范例的研究进展，其次描述了ＧＫＤ－ＡＰＳ所涉及的基本概念及所实现的通讯原语的操作语义，然后给出了系统的构成及主要实现技术，最后介绍了ＧＫＤ－ＡＰＳ所提供的智能体操作原语。     

ACUN理论一般合一化问题的合一化算法

ACUN理论是异或算子代数性质的刻画。基于联合理论合一化问题的优化分解算法和高斯消元法,本文给出了ACUN理论一般合一化问题的合一化算法。     

基于Horn逻辑扩展模型的时间敏感安全协议验证

分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法,针对它们在验证时间敏感安全协议时的不足,提出了带时间约束的安全协议的Horn逻辑扩展模型和修改版本的安全协议验证方法,并给出了相应的定义和定理,使得带时间约束的安全协议的Horn逻辑扩展模型和修改版本的安全协议验证能够分析依赖时间的安全协议的安全性质.通过在验证中加入时间约束条件,得到了大嘴青蛙协议的攻击序列,并可从约束条件中导出避免攻击的条件.     

基于TLA＋的BRP协议规约及验证

BRP协议是为不可靠信道上传送大数据包文件设计的工业协议。该协议的正确性依赖于各部件实时方面的假设。本文主要阐述了使用时序规约语言TLA＋对BRP协议进行规约和验证的过程。首先通过自然语言非形式化地描述BRP协议的基本原理和需求，在此基础上建立了BRP的形式化模型，利用TLA＋先对不考虑实时要求的BRP进行规约，然后添加实时约束获得BRP完整的规约，最后使用模型检验器TLC验证BRP协议的各种性质。     

安全协议的扩展Horn逻辑模型及其验证方法

分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法，针对它们构造不满足安全性质的安全协议反例的不足，提出了安全协议的扩展Horn逻辑模型和修改版本的安全协议验证方法，使得能够从安全协议的扩展Horn逻辑模型和修改版本的安全协议验证过程中自动构造不满足安全性质的安全协议反例．在基于函数式编程语言Objective Carol开发的安全协议验证工具SPVT中，实现了上述算法，验证了算法的正确性．