一种面向法治活动的句群级语境形式化方法

为了使计算机获得语境中包含的知识,必须对语境进行形式化描述.文中采用演绎的方法,以概念树"法治"为例,根据概念层次网络理论(HNC)世界知识的描述,设计了法治活动的领域句类表示式,将法治领域世界知识融人其中,从而使计算机获得先验知识.然后,结合真实语料分析演示了领域句类表示式对句群分析和语境单元萃取的作用,分析结果证明了领域句类表示式的适用性.最后,结合语境形式化的相关理论,讨论了语境的可计算性和语境知识表示方法,表明领域句类是计算机获取和使用语境知识的有效方法.     

面向Java的实用别名分析技术

别名分析对程序分析起着十分重要的作用,不进行别名分析或分析 算法选择不当,可能会影响分析结果的可信度,甚至会导致分析析完全不正确,因此给出了一种适用于Ｊａｖａ程序的别名分析技术,并给出了分析算法的形式化描述。     

单字动词组合处理规则的计算机实现*

以HNC理论的概念基元符号体系与句类体系为基础,探索分析了汉语中单字动词组合处理的特点及其句类特征,总结形成了处理规则。在BNF范式和产生式规则的基础上,对处理规则进行了形式化,并在计算机程序中实现了对规则的解释与执行。最后在一定量的语料中进行了规则执行测试,并给出了测试结果。     

可视程序设计语言形式化规范的研究

在计算机领域引入程序可视化技术，把图形技术融进程序设计中，其目的在于减少人与机器交流的故障。首先简述可视程序设计的基本概念，然后介绍可视程序设计语言的形式化描述，如图形系统的形式化规范，图标操作符，图标谗句的语法与语义分析描述。     

多策略汉语句子时间分析与英译

提出了汉语时间信息的新分类和时间模式的概念,基于时间模式对汉语句子的时间信息进行形式化,构建汉语句子的词汇信息和语法信息时间模式库;提出多策略汉语句子时间分析和英译方法,将汉语单句时间分析算法、汉语关联词语标记句时间分析算法、类虚拟语气句时间分析算法和篇章信息识别规则相结合。实验表明该方法能有效解决汉英机器翻译中汉语句子时间分析和英译问题。     

句间回指模糊的多层次消解模型

句间回指消解是当前中文信息处理的一个重要研究课题,直接从语义和语用入手,以法律文本为语料来源,对句间回指进行形式化描述和消解,服务于计算机句群自动理解。概念基元是“显微镜”,看清指代语与先行语的微观语义联系;句类是“放大镜”,将指代语和先行语纳入57组基本句类中进行关联;语境单元则是“望远镜”,为指代语和先行语提供宏观的语境知识。语料考察结果表明,这一多层次的消解模型对实现句间回指消解是有效的。     

面向汉英机器翻译的专利文献小句变换研究

专利文献的自动翻译是机器翻译的一个重要应用领域,复杂长句的翻译是汉英机器翻译的难点。本研究期望找出汉英复杂长句中小句变换的形式化转换规则。汉语复杂长句中会包含多个小句,这些小句都是独立存在的,但翻译成英语时,一般只有一个核一心小句,其他小句都变换成doing、todo、从句或短语等其它形式。文中以1300句汉英双语专利文献语料为研究对象,对汉语中的小句翻译为英语的变换情况进行分类研究,从小句句间关系、共享关系的角度出发,描述激活特征,并按五种变换方式分类,提出了十二条变换规则,小规模语料实验结果证明规则可行有效。下一步工作需要扩充研究语料,对语料进行更深入的挖掘和分析,在更大规模语料中验证规则的实用性。     

满足对应性属性的平台配置证明

针对完整性报告协议（IRP）存在局部和全局攻击的安全隐患,对StatVerif进行语法扩展,增加了与完整性度量相关的构造算子和析构算子,通过对平台配置证明（PCA）安全进行分析,发现其存在的局部攻击和全局攻击,包括通过未授权命令对平台配置寄存器和存储度量日志进行篡改。对攻击者能力进行了建模,详细说明了攻击者如何通过构造子和析构子形成知识,进而对平台配置证明进行攻击。最后,在平台配置证明不满足对应性属性的情况下,从理论上证明了攻击序列的存在,并给出了平台配置证明满足局部可靠和全局可靠的条件,通过形式化验证工具Proverif证明了命题的合理性。     

安全协议的形式化方法概述

介绍了安全协议的形式化分析思路,阐述了安全协议形式化描述、需求、验证及设计四个方面的研究状况和它们的基本原理,并对常用的几种形式化验证技术的优缺点进行了分析,最后针对形式化技术在该领域的发展前景提出了自己的见解。     

从形式化式样出发的实时控制软件开发

形式化语言能够对软件的功能进行精确的描述,在实时控制软件中引入形式化语言描述是必要的也是可能的本文介绍了形式化式样语言VDM-SL(Vienna Development Method-Specification Language),用VDM-SL给出了一个小型控制软件的形式化描述。基于形式化式样描述,提出了从形式化式样出发的控制软件开发最后就形式化语言应用于软件描述的前景进行了分析,同时指出了形式化语言和工具的不足。     

Syntactic Calculus with Dependent Types

The aim of this study is to look at the the syntactic calculus of Bar-Hillel and Lambek, including semantic interpretation, from the point of view of constructive type theory. The syntactic calculus is given a formalization that makes it possible to implement it in a type-theoretical proof editor. Such an implementation combines formal syntax and formal semantics, and makes the type-theoretical tools of automatic and interactive reasoning available in grammar.In the formalization, the use of the dependent types of constructive type theory is essential. Dependent types are already needed in the semantics of ordinary Lambek calculus. But they also suggest some natural extensions of the calculus, which are applied to the treatment of morphosyntactic dependencies and to an analysis of selectional restrictions. Finally, directed dependent function types are introduced, corresponding to the types of constructive type theory.Two alternative formalizations are given: one using syntax trees, like Montague grammar, and one dispensing with them, like the theory called minimalistic by Morrill. The syntax tree approach is presented as the main alternative, because it makes it possible to embed the calculus in a more extensive Montague-style grammar.     

Formalisation method for the text expressed knowledge

This paper describes a method of knowledge representation as a set of text expressed statements. The method is based on the identification of word-categories/phrases and their semantic relationships within the observed statement. Furthermore, the identification of semantic relationships between words/phrases using wh-questions that clarify the role of the word/phrase in the relationship is described. A conceptual model of the computer system based on the formalization method of text-expressed knowledge is proposed. The subsystem text formalization is described in detail, especially its parts: syntactic analysis of the sentence, sentence formalization, phrase structure grammar and lexicon. The phrase structure grammar is formed by induction and it is used to generate the language of the formalized notation of a sentence. The derivation of grammar is based on the simple phrase structure grammar which was used for the syntactical analysis of informal language notation. In its base, the suggested method translates sentences of the informal language into formal language sentences which are generated by the derivated phrase structure grammar. Current limitations of the method that also set the path of its further development are shown. Next concrete steps in the development of the method are also described.     

基于句式结构的汉语图解析句法设计

梳理了汉语语法学界对“句式”这一术语的认识分歧;从中文信息处理角度分析了当前本领域句法分析和树库构建缺乏句式结构的现状;对黎氏语法形式化研究作了一个最新的综述,指出其在句式结构方面的优势和仍存在的不足;以黎氏语法图解法为原型改造设计出一种新型的汉语图解析句法,具体包括图形化的句法结构表示和结构化的XML存储格式。     

Meta-modelling based assembly techniques for situational method engineering

Method engineering for information system development is the discipline to construct new advanced development methods from parts of existing methods, called method fragments. To achieve this objective, we need to clarify how to model the existing methods and how to assemble method fragments into new project-specific methods, so-called situational methods. Especially, to produce meaningful methods, we should impose some constraints or rules on method assembly processes. In this paper, we propose a framework for hierarchical method modelling (meta-modelling) from three orthogonal dimensions: perspectives, abstraction and granularity. According to each dimension, methods and/or method fragments are hierarchically modelled and classified. Furthermore, we present a method assembly mechanism and its formalization as a set of rules. These rules are both syntactic and semantic constraints and presented in first order predicate logic so that they can play an important role in the assembly process of syntactically and semantically meaningful methods from existing method fragments. The benefit of our technique is illustrated by an example of method assembly, namely the integration of the Object Model and Harel's Statechart into Objectcharts.     

R-演算中若干问题的研究

李未教授提出了R-演算系统,它是形式理论的修正演算系统,是OPEN过程模式和GUINA过程模式的基础.R-演算在这2种过程模式中的核心作用是,当一个形式理论与事实产生矛盾时,找出矛盾的必要前提,从而获得一个协调的子理论.通过3种不同的方法细致刻画R-演算的基本概念"必要前提",第1种方法来自R-演算,第2种方法基于极大协调子集与极小非协调子集的,最后一种方法是对于R-必要前提的归纳定义.通过比较这3种方法,指出各自的优缺点,并从第3种方法推演出一个可靠并且相对完全的系统.在比较这3种方法的同时,还细致地探讨了R-终止式的上下界以及极大协调子集的不可枚举性.其中极大协调的不可枚举性在一定程度上表明了不存在一种同时满足可靠并且完全的系统.     

机器翻译中句法分析的设计与实现

论述了英汉机器翻译中句法分析的设计与实现方法。首先阐述了编译原理中句法分析的相关理论，并以此理论为依据提出了机器翻译中句法分析的具体实现。实现过程中，采用部分分析的思想，将一个句子划分为多个语法成分，分别对各语法成分进行分析，从而完成对待翻译句子的句法分析，给出句法树。     

Temporal predicate transformers and fair termination

Summary It is usually assumed that implementations of nondeterministic programs may resolve the nondeterminacy arbitrarily. In some circumstances, however, we may wish to assume that the implementation is in some sense fair, by which we mean that in its long-term behaviour it does not show undue bias in forever favouring some nondeterministic choices over others. Under the assumption of fairness many otherwise failing programs become terminating. We construct various predicate transformer semantics of such fairly-terminating programs. The approach is based on formulating the familiar temporal operators always, eventually, and infinitely often as predicate transformers. We use these operators to construct a framework that accommodates many kinds of fairness, including varieties of socalled weak and strong fairness in both their all-levels and top-level forms. Our formalization of the notion of fairness does not exploit the syntactic shape of programs, and allows the familiar nondeterminacy and fair nondeterminacy to be arbitrarily combined in the one program. Invariance theorems for reasoning about fairly terminating programs are proved. The semantics admits probabilistic implementations provided that unbounded fairness is excluded.     

Formalizing an Analytic Proof of the Prime Number Theorem

We describe the computer formalization of a complex-analytic proof of the Prime Number Theorem (PNT), a classic result from number theory characterizing the asymptotic density of the primes. The formalization, conducted using the HOL Light theorem prover, proceeds from the most basic axioms for mathematics yet builds from that foundation to develop the necessary analytic machinery including Cauchy’s integral formula, so that we are able to formalize a direct, modern and elegant proof instead of the more involved ‘elementary’ Erdös-Selberg argument. As well as setting the work in context and describing the highlights of the formalization, we analyze the relationship between the formal proof and its informal counterpart and so attempt to derive some general lessons about the formalization of mathematics.