传值系统的互模拟与谓词等式系

National Natural Science Foundation of China; Public Administration and Civil Service Bureau of Macau SAR; Companhia de Telecomunicacoes de Macau S.A.R.L.; Macau SAR Government Tourist Office

带复杂数据结构的模型检测工具

模型检测是近二十几年来最成功的自动验证技术之一,而模型检测工具的开发是将模型检测和实际相结合的关键.为了有效地对涉及到复杂数据类型的并发传值系统进行模型检测,总结了以扩展的带赋值符号迁移图和模态图分别作为并发系统和逻辑公式的语义模型来实现模型检测工具的工作,特别是将复杂数据结构引入传值进程定义语言和带赋值符号迁移图.同时结合实际例子说明模型检测工具的有效性.

谓词μ演算和模态图的语义一致性

模态图是谓词μ演算的一种有效的图形表示形式。证明了谓词μ演算和模态图的语义一致性，详细讨论了谓词μ演算公式、嵌套谓词等式系和模态图之间的关系，并给出了一种优化的从线性公式到嵌套谓词等式系的转换算法。

面向传值进程的谓词μ-演算与FO(HML)的完备推演系统

National Natural Science Foundation of China; Public Administration and Civil Service Bureau of Macau SAR; Companhia de Telecomunicacoes de Macau S.A.R.L.; Macau SAR Government Tourist Office

嵌套谓词等式系与弱互模拟

National Natural Science Foundation of China; Public Administration and Civil Service Bureau of Macau SAR; Companhia de Telecomunicacoes de Macau S.A.R.L.; Macau SAR Government Tourist Office

Alkali metal ions transfer across a water/1,2-dichloroethane interface facilitated by a novel monoaza-B15C5 derivative

In this paper, a novel monoaza-B15C5 derivative, N-(2-tosylamino)-isopentyl-monoaza-15-crown-5 (L), is used as an ionophore to facilitate alkali metal cations transfer across a water/1,2-dichloroethane (W/DCE) interface. Well-defined voltammetric behaviors are observed at the polarized W/DCE interfaces supported at micro- and nano-pipets except Cs+. The diffusion coefficient of this ionophore in the DCE phase is calculated to be equal to (3.3+/-0.2) x 10(-6) cm(2) s(-1). The experimental results indicate that a 1:1 (metal: ionophore) complex is formed at the interface with a TIC/TID mechanism. The selectivity of this ionophore towards alkali ions follows the sequence Na+ > Li+ > K+ > Rb+ > Cs+. The logarithm of the association constants (log beta(1)(0)) of the LiL+, NaL+, KL+ and RbL+ complexes in the DCE phase are calculated to be 10.6, 11.6, 9.0 and 7.1, respectively. The kinetic parameters are determined by steady-state voltammograms using nanopipets. The standard rate constants (k(0)) for Li+, Na+, K+ and Rb+ transfers facilitated by L are 0.54+/-0.05, 0.63+/-0.09, 0.51+/-0.04 and 0.46+/-0.06 cm s(-1), respectively. The pH values of aqueous solution have little effect on the electrochemical behaviors of these facilitated processes. The results predicate that this new type of ionophore might be useful to fabricate electrochemical sensor of sodium ion.

基于谓词不变性的状态反馈控制在机器人遥操作中的应用

传统的基于事件遥操作系统虽然巧妙地避开了变化时延问题[8] ,但是它具有“走走停停”的特点 ,即机器人将当前状态发送出去之后直到操作者的下一个指令到来之前机器人必须保证状态没有变化。对此本文首次提出了利用基于谓词不变性的状态反馈控制来对原有的方法进行改进 ,使机器人能够对动态环境具有适应性

改革对教师工作生活质量影响的跨文化比较研究

From the organizational behavior point, this study initially explored how factors of educational changes influenced on teachers. This study adapted the questionnaire made up by Consortium for Cross-Culture Research in Education (CCCRE), by cooperating with other countries, interviewed 513 teachers in nine countries. The main results are as follows: 1. Factors of educational changes include: domain, origin, objective, teachers' role, and timetable. Comparative results show: More similarities than differences tend to be presented in five factors. The detail results are: in domain, it mainly involves teaching change and learning outcomes change; in origin, the educational change most teachers participated was initialed by government; in role, teachers more act as the implementer; in timetable, gradual development is the chief characteristic. 2. The domain of change, origin and teachers' role has a significant impact on the quality of worklife of teachers, but timetable of change has not. The further study about the influence of educational origin on the quality of worklife of teachers shows: Changes of teachers' time -using, professional development were significantly impacted by the origin of education, and there is a significant difference in the change of time-using among nine countries. 3. Change on students, change on teachers' relationship are two important factors to impact the teachers' evaluation about educational change. But the teachers' evaluation, teaching age and the change on relationship are valid factors to predicate teachers participate in next educational change. 4. Compared with the educational change of other eight countries, the change in school system management and the change in learning outcomes are more carried on in China. There is no significance about other factors between China and overall nine countries. In China, the educational change has a more positive impact on teachers' time-using and professional development, but professional development is also a important factor to impact teachers' evaluation on change; however there is a negative relationship between the Chinese teachers' evaluation and the teachers' participation in next change.

Taxonomic Syntax for First-Order Inference

Most knowledge representation languages are based on classes and taxonomic relationships between classes. Taxonomic hierarchies without defaults or exceptions are semantically equivalent to a collection of formulas in first order predicate calculus. Although designers of knowledge representation languages often express an intuitive feeling that there must be some advantage to representing facts as taxonomic relationships rather than first order formulas, there are few, if any, technical results supporting this intuition. We attempt to remedy this situation by presenting a taxonomic syntax for first order predicate calculus and a series of theorems that support the claim that taxonomic syntax is superior to classical syntax.

Toward a Theory of Representation Design

This research is concerned with designing representations for analytical reasoning problems (of the sort found on the GRE and LSAT). These problems test the ability to draw logical conclusions. A computer program was developed that takes as input a straightforward predicate calculus translation of a problem, requests additional information if necessary, decides what to represent and how, designs representations capturing the constraints of the problem, and creates and executes a LISP program that uses those representations to produce a solution. Even though these problems are typically difficult for theorem provers to solve, the LISP program that uses the designed representations is very efficient.

TYPICAL: A Knowledge Representation System for Automated Discovery and Inference

TYPICAL is a package for describing and making automatic inferences about a broad class of SCHEME predicate functions. These functions, called types following popular usage, delineate classes of primitive SCHEME objects, composite data structures, and abstract descriptions. TYPICAL types are generated by an extensible combinator language from either existing types or primitive terminals. These generated types are located in a lattice of predicate subsumption which captures necessary entailment between types; if satisfaction of one type necessarily entail satisfaction of another, the first type is below the second in the lattice. The inferences make by TYPICAL computes the position of the new definition within the lattice and establishes it there. This information is then accessible to both later inferences and other programs (reasoning systems, code analyzers, etc) which may need the information for their own purposes. TYPICAL was developed as a representation language for the discovery program Cyrano; particular examples are given of TYPICAL's application in the Cyrano program.

Assimilation of New Information by a Natural Language Understanding System

This work describes a program, called TOPLE, which uses a procedural model of the world to understand simple declarative sentences. It accepts sentences in a modified predicate calculus symbolism, and uses plausible reasoning to visualize scenes, resolve ambiguous pronoun and noun phrase references, explain events, and make conditional predications. Because it does plausible deduction, with tentative conclusions, it must contain a formalism for describing its reasons for its conclusions and what the alternatives are. When an inconsistency is detected in its world model, it uses its recorded information to resolve it, one way or another. It uses simulation techniques to make deductions about creatures motivation and behavior, assuming they are goal-directed beings like itself.

SIR: A Computer Program for Semantic Information Retrieval

SIR is a computer system, programmed in the LISP language, which accepts information and answers questions expressed in a restricted form of English. This system demonstrates what can reasonably be called an ability to "understand" semantic information. SIR's semantic and deductive ability is based on the construction of an internal model, which uses word associations and property lists, for the relational information normally conveyed in conversational statements. A format-matching procedure extracts semantic content from English sentences. If an input sentence is declarative, the system adds appropriate information to the model. If an input sentence is a question, the system searches the model until it either finds the answer or determines why it cannot find the answer. In all cases SIR reports its conclusions. The system has some capacity to recognize exceptions to general rules, resolve certain semantic ambiguities, and modify its model structure in order to save computer memory space. Judging from its conversational ability, SIR, is a first step toward intelligent man-machine communication. The author proposes a next step by describing how to construct a more general system which is less complex and yet more powerful than SIR. This proposed system contains a generalized version of the SIR model, a formal logical system called SIR1, and a computer program for testing the truth of SIR1 statements with respect to the generalized model by using partial proof procedures in the predicate calculus. The thesis also describes the formal properties of SIR1 and how they relate to the logical structure of SIR.

Determining the Scope of English Quantifiers

How can one represent the meaning of English sentences in a formal logical notation such that the translation of English into this logical form is simple and general? This report answers this question for a particular kind of meaning, namely quantifier scope, and for a particular part of the translation, namely the syntactic influence on the translation. Rules are presented which predict, for example, that the sentence: Everyone in this room speaks at least two languages. has the quantifier scope AE in standard predicate calculus, while the sentence: At lease two languages are spoken by everyone in this room. has the quantifier scope EA. Three different logical forms are presented, and their translation rules are examined. One of the logical forms is predicate calculus. The translation rules for it were developed by Robert May (May 19 77). The other two logical forms are Skolem form and a simple computer programming language. The translation rules for these two logical forms are new. All three sets of translation rules are shown to be general, in the sense that the same rules express the constraints that syntax imposes on certain other linguistic phenomena. For example, the rules that constrain the translation into Skolem form are shown to constrain definite np anaphora as well. A large body of carefully collected data is presented, and used to assess the empirical accuracy of each of the theories. None of the three theories is vastly superior to the others. However, the report concludes by suggesting that a combination of the two newer theories would have the greatest generality and the highest empirical accuracy.

Using a logical model to predict the growth of yeast

Whelan, K. E. and King, R. D. Using a logical model to predict the growth of yeast. BMC Bioinformatics 2008, 9:97