由一阶逻辑公式得到命题逻辑可满足性问题实例

命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为 SAT 问题.为了利用现有的高效 SAT工具,提出了一种从一阶逻辑公式生成 SAT 问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题.

基于一阶迁移系统的限界模型检测工具实现

基于布尔可满足性(SAT)的限界模型检测是一种高效的模型检测方法，它具有快速查错，反例最小化等特点，已经成为学术界和工业界关注的热点。近些年出现了很多集成限界模型检测算法的验证工具，如ITC-IRST、卡内基梅隆大学(CMU)等多家科研机构联合开发的NuSMV工具；加利福尼亚大学伯克莱分校(UC Berkeley)、科罗拉多大学博尔德分校(CU Boulder)联合开发的VIS工具等。因此目前对于限界模型检测方法的研究和相关工具的设计与开发具有重要而广泛的意义。在进行限界模型检测的建模过程中，不同的工具采用了自定义的建模语言。如经典工具SPIN采用的建模语言是Promela语言，NuSMV采用的是自定义的NuSMV语言。随着系统验证规模的不断增大，建模语言的特点将会直接影响到建模的效率。例如采用NuSMV语言去建立一个网络通信协议模型会显得比较复杂和耗时，应用NuSMV语言去描述一个简单的数据链路层网络协议ABP协议(Alternating Bit Protocol)就不如采用Promela语言去描述显得直观和自然。 为了简化在限界模型检测过程中模型的建立过程，本文给出了一种采用基于一阶迁移系统语言描述的模型建立方法，并在一阶迁移系统语言中实现了通道的功能，从而增强了描述能力。在此基础上完成了一个以基于插值和k步归纳限界验证算法为核心的模型检测工具(BMCF)。最后利用该工具对常见的互斥协议，简单数据传输协议的性质进行了分析与验证。结果表明，利用该工具对系统进行建模具有方便直观的特点，并借助实现的验证算法能高效的检验安全性质的正确性，如果性质不成立工具会给出反例提示。

可满足性问题研究

数理逻辑是计算机科学的基础，而逻辑公式的可满足性问题是计算机科学和人工智能领域中的一个著名而又重要的问题。它在计算机科学和人工智能研究中有广泛的应用。本文将重点介绍实际可用的判定算法及其相关技术。 本文的研究分两大方向，分别是命题逻辑的可满足性问题研究和一阶逻辑的可满足性问题研究。命题逻辑的可满足性问题（Satisfiability Problem）是一个历史悠久的问题，一般简称为 SAT问题。SAT 问题的求解算法有两大类，分别是确定性算法和非确定性算法。本文只研究确定性算法的相关内容，尤其是如何进行剪枝。我们充分调研了SAT求解算法和求解工具的相关知识，在此基础上，提出了local Lemma 这个剪枝技术，该技术可以更加充分地挖掘剪枝信息，达到进行更多剪枝的目的。 在一阶逻辑的可满足性问题研究方面，本文采取直接搜索可行的一阶逻辑模型的方法研究有限论域上的一阶逻辑的可满足性问题。该方法本质上就是深度优先的回溯搜索。因此，我们的研究重点就是如何找到问题的更高效的一阶逻辑的表示以及如何采用启发式的方式进行剪枝。在这个问题上，我的主要工作有两个：一个是模型搜索中适用于谓词的同构消去技术，包括Row by Row策略和Ramsey Number 策略两个技术；另一个是 DASH（Decision Assignment Scheme Heuristic），用来在生成有限模型的时候边搜索边消除同构子空间。DASH 能用近乎零代价保证输出的模型都是互不同构的。这两个技术都是基于有限论域中的元素的固有对称性，换言之，就是需要有限论域中的元素是两两可交换的。 在已有的成果的基础上，我们又尝试使用它们去求解一些数学中的实际问题，如拟群拉丁方，有限射影平面，正交拉丁方（组）等。我们给出了在这几个方面的一些尝试和初步结果，包括一个重要的定理和若干效率提高了几个数量级的改进。 值得一提的是，和马菲菲共同提出的横截矩阵（Transversal Matrix）概念是一个新颖的成果，使得正交拉丁方的表示和求解取得了明显的改进。在这个概念的基础上，进一步给出了几个定理，进行了理论上的拓展。实验数据表明，我们的求解途径和技术能有效解决拉丁方相关的问题。

组合对象的搜索算法研究

现实世界中的大量问题涉及如何安排有限个离散的基本对象，使之满足特定约束，这类问题可通称为组合问题。本论文主要研究复杂的组合对象的存在性问题。我们特别关注较难求解的组合问题，从算法复杂度上来说，至少是NP难的。由于这些组合对象相应的约束一般都不太容易满足，因此局部搜索等非完备算法方法常常失效。我们致力于研究高效的完备搜索算法，能够在庞大的搜索空间中精准地找到解，当解不存在时，也能够给出确定性的回答。 作者在博士期间的工作可分为两部分：组合数学问题的自动求解和线性约束上的可满足性模理论的体积求解。 我们系统化地研究了组合数学问题的计算机求解，这部分研究包括三大类问题：幂等拟群的大集问题、正交拉丁方和正交数组。这些问题的共同特点是，要寻找的不是一个复杂的组合对象，而是一系列复杂的组合对象，这些对象相互之间还要满足一定的约束。这样一来，搜索空间比寻找单独的一个组合对象要庞大很多倍，问题的难度也大大增加了。对于每一类问题，我们都通过深入研究其结构特征，提出了有效的问题表示方法和搜索方法，发展了一系列新颖的消除同构技术来降低搜索空间，在搜索中我们应用了自动推理最新的技术和工具，如高效的一阶逻辑模型产生器和命题逻辑求解器等，取得了较好的效果。具体来说，我们的工作包括以下三点： (1) n阶幂等拟群的大集问题需要寻找n-2个不相交的幂等拟群，这比寻找单个的满足特定性质的拟群要困难的多。我们设计了约束分割的策略，解决了幂等拟群大集上的一系列开放性问题，特别是得出了LSPQ(11)不存在的结论。我们的方法不但可以回答特定的大集是否存在，还能够确定相互不相交的拟群的最大个数。这些数学结果对朱烈教授等数学家很有意义，并被收入``HandBook of Satisfiability"一书中。 (2) 正交拉丁方的存在性是组合数学中著名的问题。我们利用一阶逻辑有限模型产生器对该问题进行了尝试，提出了一种新的建模方法，称为横截建模，其效果比直接建模方法提高了若干个数量级。同时，我们也提出了一种新的打破对称策略。 (3) 正交数组是一种重要的组合数学结构，可用于软件组件的集成测试。我们设计了一个搜索正交数组的完备性算法，并提出了一些新颖的打破对称技术。与当前的其它工作不同，我们的算法是普适性的，对输入OA参数无任何限制，并且当搜索完成后总能得到确定性的答案。实验表明，我们的工具BOAS在搜索强度为3及其以上的正交数组时非常高效，而用传统的数学方法构造这些数组则很困难，局部搜索算法也对这些数组常常失效。而且，BOAS能够轻易地解决一批对于其它完备算法来说非常难的实例。 我们研究的第二个方面是线性理论上的SMT实例的体积计算问题。关于各类逻辑和约束语言的可满足性问题有大量的研究工作，比如SAT和可满足性模理论（SMT），另一方面，判定问题的计数版本在自动推理中也非常重要。我们研究了SMT的计数版本，即对给定的SMT实例（更精确地说，线性算术约束的布尔组合）如何计算解的个数，或者是说如何计算解空间的体积。这一问题同时扩展了命题逻辑的模型计数问题和凸多面体的体积计算问题。SMT实例的体积计算在许多领域都有潜在的应用价值，比如程序分析与验证和近似推理，但目前还没有相关的研究工作。我们首次研究了这一问题，提出了一个高效的体积计算方法——逐簇法，我们的算法集成了SMT求解中的最新技术。我们的原型工具在随机实例上产生了较好的效果，并可应用在实际的程序实例中，以寻找热门路径。

安培酶电极的新固定化方法和用途扩展研究

1．用溶胶-凝胶方法制备了一种新型的有机-无机杂交材料，并用这种材料制备了过氧化物酶安培酶电极。用富里叶变换红外光谱和石英晶体微天平对这种有机-无机杂交材料和用这种材料制备的酶膜进行了表征。以亚铁氰化钾为媒介体考察了传感器的电化学行为。用计时安培方法优化了pH和工作电位。传感器的响应时间为10s，线性范围的上限达3.4 mM，检测限为5 * 10~(-7)M。传感器具有高的灵敏度和好的长期稳定性。另外，还把传感器用于流动注射分析和实际样品分析来评估传感器的性能。2．利用有机修饰的溶胶-凝胶材料的优点，制备含磺酸基的功能化的溶胶，用无机-有机杂交手段制备功能化的薄膜(FIOHM)，进而制备了媒介体型过氧化氢安培生物传感器。麦尔多拉兰(MDB)通过离子交换作用被固定在膜中，MDB在FIOHM膜中的循环伏安行为比溶液中的MDB的循环伏安行为更为可逆，因而适合于作媒介体。由于磺酸基的供电子能力，MDB分子的电子密度增加，因而就变得易于氧化而难于还原，表现为阴极峰和阳极峰峰电位的负移。这是第一次用溶胶-凝胶方法制备的磺化无机-有机复合材料制备媒介体型过氧化氢传感器。响应时间小于25 s。线性范围上限达0.6mM。高的灵敏度75 nA·μM·cm~(-2)是由于高的MDB载量。检测限为0.9 μM。传感器具有灵敏的响应和满意的稳定性。3．实验证明自身成胶的接枝共聚物PVA-g-PVP是酪氨酸酶的好的固定化材料。三维氢键网络把酶包埋在聚合物膜中。这种固定化方法简单温和。4-乙烯基吡啶组分增强了膜在电极表面的附着力，所以传感器在流动体系中稳定且重现性好。酶膜组成可以调节以得到好的灵敏度或宽的线性范围以满足不同的分析要求。传感器表现出很好的重现性，稳定性和灵敏的响应。传感器在亲水有机溶剂中的线性范围加宽。制备了安培型酚传感器。固定化材料是引入了接枝共聚物PVA-g-PVP的溶胶-凝胶复合膜。酪氨酸酶有效地固定在复合膜中。对这一无机-有机复合杂交材料进行了优化。酪氨酸酶在溶胶-凝胶膜中保持了其活性，在0V(Ag/AgCl，Sat．KCl)测定了其响应。讨论了pH、氧浓度、温度对响应的影响，考察了传感器的稳定性。酶电极对儿茶酚，苯酚，对-甲苯酚的灵敏度分别为59.6，23.1，39.4μA／mM。酶电极在4℃干态保存，间歇测定3周后，其响应为初始值的73％，稳定性好于接枝共聚物PVA-g-PVP为载体的酪氨酸酶电极。5．首次用安培酶电极定量测定极性有机溶剂。初步实验证实了用酪氨酸酶电极安培法定量惰性的极性有机溶剂的可行性。酪氨酸酶电极的制备方法简单：把酪氨酸酶和共聚物的水溶液滴涂在经过抛光的洁净的玻碳电极表面上，然后置于+4℃冰箱中干燥成膜即可。电化学还原酪氨酸酶催化氧化酚生成的醌提供探测信号。此传感器可以用于定量测定甲醇，乙醇，正丁醇，丙酮，乙腈，四氢呋喃等。该方法对某有机溶剂的检测限，灵敏度，线性范围依赖于所使用的固定化材料和底物的疏水性。对所测试的有机溶剂的响应时间小于2分钟。现场计时电流-石英晶体微天平实验证实了其响应机理：加入的有机溶剂富集底物探针酚，因而降低了酶膜中的酚的浓度。增加底物探针的浓度可以增加检测的灵敏度，因而降低检测限。此方法检测极性有机溶剂的特点是简单，容易，迅速。用酪氨酸酶电极安培定量测定惰性的极性有机溶剂，大大扩展了酶电极的应用范围。用这种检测方法的优点是，可以定量测定那些还没有发现专一性的酶来构造生物传感器的有机溶剂。6．生物传感器的研究中最重要和最基本的问题是酶的固定化。我们小组提出了用低温水凝胶固定化酶方法构造有机相酶电极，但是低温水凝胶与酶的相互作用仍不清楚。我们利用肼类化合物作为探针，研究了辣根过氧化物酶与低温水凝胶的相互作用。常用的羧基捕捉剂肼和对血红素边缘有高度选择性的甲基肼不能很快地明显抑制固定在低温水凝胶中的辣根过氧化物酶的活性。原因是辣根过氧化物酶的构象可能被低温水凝胶锁定，辣根过氧化物酶的羧基和其血红素的边缘被低温水凝胶保护而免受肼类化合物的进攻。作为比较，肼类化合物与吸附在石墨电极上的辣根过氧化物酶的相互作用也用稳态电流响应和循环伏安进行了研究。对水凝胶固定化酶方法．提出了酶电极响应的动力学参数的初步理论解释，其中低温水凝胶层的厚度和电子媒介体的扩散系数不影响米氏常数K_M，但这些参数显著影响饱和响应电流I_(max)。7．六氰合铁钴(II)膜修饰的玻碳电极用于构造电流型葡萄糖传感器。以六氰合铁钴(II)膜电化学催化还原酶促反应过程中产生的过氧化氢为分析信号。明胶作为固定化材料，外涂Nafion膜。低的适加电位避免电化学氧化抗坏血酸、尿酸等干扰物。Nafion涂层靠静电斥力，阻止这些阴离子干扰物到达电极表面。得到了宽的线性范围，给出分析性能参数，进行了动力学分析。

Kinetics of dissociative water adsorption on stepped Si(001), on Si(115), Si(113), Si(5,5,12) and Si(112)

We present photoelectron spectroscopic and low energy electron diffraction measurements of water adsorption on flat Si samples of the orientations (001), (115), (113), (5,5,12) and (112) as well as on curved samples covering continuously the ranges (001)-(117) and (113)-(5,5,12)-(112). On all orientations, water adsorption is dissociative (OH and H) and non-destructive. On Si(001) the sticking coefficient S and the saturation coverage Theta(sat) are largest. On Si(001) and for small miscuts in the [110]-azimuth, S is constant nearly up to saturation which proves that the kinetics involves a weakly bound mobile precursor state. For (001)-vicinals with high miscut angles (9-13 degrees), the step structure breaks down, the precursor mobility is affected and the adsorption kinetics changed. On (115), (113), (5,5,12) and (112), the values of S and Theta(sat) are smaller which indicates that not all sites are able to dissociate and bind water. For (113) the shape of the adsorption curves Theta versus exposure shows the existence of two adsorption processes, one with mobile precursor kinetics and one with Langmuir-like kinetics. On (5,5,12), two processes with mobile precursor kinetics are observed which are ascribed to adsorption on different surface regions within the large surface unit cell. From the corresponding values of S and Theta(sat), data for structure models are deduced. (C) 1997 Elsevier Science B.V.

改进的以SMT为基础的实时系统限界模型检测

基于SAT的限界模型检测在处理实时系统时具有很高的复杂度.SMT求解器在计算可满足性的同时,还能处理算术和其他可判定性理论.在对实时系统进行检测时,用SMT求解器代替SAT求解器,系统里的时钟就可以用整型或实型变量表示,时钟约束则可以直接表示成线性算术表达式,从而使整个检测过程更加高效.带时间参数的计算树逻辑(timed computation tree logic,简称TCTL)被用来描述实时系统里的性质.同时,还对检测方法作了相应的改进.

Simple preparation method of Pd nanoparticles on an Au electrode and its catalysis for dioxygen reduction

A simple method for the fabrication of Pd nanoparticles is described. The three-dimensional Pd nanoparticle films are directly formed on a gold electrode surface by simple electrodeposition at -200 mV from a solution of 1 M H2SO4+0.01 mM K2PdCl4. X-Ray photoelectron spectroscopy verifies the constant composition of the Pd nanoparticle films. Atomic force microscopy proves that the as-prepared Pd nanoparticles are uniformly distributed with an average particle diameter of 45-60 nm. It is confirmed that the morphology of the Pd nanoparticle films are correlated with the electrodeposition time and the state of the Au substrate. The resulting Pd-nanoparticle-film-modified electrode possesses high catalytic activity for the reduction of dissolved oxygen in 0.1 M KCl solution. Freshly prepared Pd nanoparticles can catalyze the reduction of O-2 by a 4-electron process at -200 mV in 0.1 M KCl, but this system is not very stable. The cathodic peaks corresponding to the reduction of O-2 gradually decrease with potential cycling and at last reach a steady state. Then two well-defined reduction peaks are observed at -390 and -600 mV vs. Ag/AgCl/KCl (sat.). Those two peaks correspond to a 2-step process for the 4-electron reduction pathway of O-2 in this neutral medium.

Silica sol-gel composite film as an encapsulation matrix for the construction of an amperometric tyrosinase-based biosensor

An amperometric tyrosinase enzyme electrode for the determination of phenols was developed by a simple and effective immobilization method using sol-gel techniques. A grafting copolymer was introduced into sol-gel solution and the composition of the resultant organic-inorganic composite material was optimized, the tyrosinase retained its activity in the sol-gel thin film and its response to several phenol compounds was determined at 0 mV vs. Ag/AgCl (sat. KCI). The dependences of the current response on pH, oxygen level and temperature were studied, and the stability of the biosensor was also evaluated. The sensitivity of the biosensor for catechol, phenol and p-cresol was 59.6, 23.1 and 39.4 muA/mM, respectively. The enzyme electrode maintained 73% of its original activity after intermittent use for three weeks when storing in a dry state at 4 degreesC. (C) 2000 Elsevier Science S.A. All rights reserved.

Electrocatalytic oxidation of hydrazines at a 4-pyridyl hydroquinone self-assembled platinum electrode and its application to amperometric detection in capillary electrophoresis

4-Pyridyl hydroquinone on a platinum electrode adsorbs through the pyridine nitrogen forming stable self-assembled layers. The electrocatalytical oxidation of hydrazines was performed by the modified electrode. The overpotential of hydrazines was decreased markedly at the self-assembled monolayer (SAM) electrode. The mechanism of hydrazine oxidation was also investigated. Amperometric detection of hydrazine under zero potential (vs Ag\AgCI\sat. KCl) was exhibited by the SAM electrode used as an electrochemical detector in a flow system. (C) 1998 Elsevier Science S.A. All rights reserved.

Electrochemical scanning tunneling microscopy and electrochemical quartz crystal microbalance study of the adsorption of phenanthraquinone accompanied by an electrochemical redox reaction on the Au electrode

In situ electrochemical scanning tunneling microscopy (ECSTM) and an electrochemical quartz crystal microbalance (EQCM) have been employed to follow the adsorption/desorption processes of phenanthraquinone (PQ sat. in 0.1 mol l(-1) HClO4, solution) accompanied with an electrochemical redox reaction on the Au electrode. The result shows that: (1) the reduced form PQH(2) adsorbed at the Au electrode and the desorption occurred when PQH(2) was oxidized to PQ; (2) the adsorption process initiates at steps or kinks which provide high active sites on the electrode surface for adsorption, and as the potential shifts to negative, a multilayer of PQH(2) may be formed at the Au electrode; (3) the reduced PQH(2) adsorbed preferentially in the area where the tip had been scanned continually; this result suggests that the tip induction may accelerate the adsorption of PQH(2) on the Au(111) electrode. Two kinds of possible reason have been discussed; (4) high resolution STM images show the strong substrate lattice information and the weak monolayer adsorbate lattice information simultaneously. The PQH(2) molecules pack into a not perfectly ordered condensed physisorbed layer at potentials of 0.1 and 0.2 V with an average lattice constant a = 11.5 +/- 0.4 Angstrom, b = 11.5 +/- 0.4 Angstrom, and gamma = 120 +/- 2 degrees; the molecular lattice is rotated with respect to the substrate lattice by about 23 +/- 2 degrees. (C) 1997 Elsevier Science S.A.

EFFECTS OF ANODIC-OXIDATION ON THE SURFACE-STRUCTURE OF HIGHLY ORIENTED PYROLYTIC-GRAPHITE REVEALED BY IN-SITU ELECTROCHEMICAL SCANNING-TUNNELING-MICROSCOPY IN H2SO4 SOLUTION

Effects of the potential of anodic oxidation and of potential cycling on the surface structure of a highly oriented pyrolytic graphite (HOPG) electrode were observed by in situ electrochemical scanning tunnelling microscopy (ECSTM) in dilute H2SO4 solution with atomic resolution. With potential cycling between -0.1 V and 1.8 V vs. Ag/AgCl (sat. KCI), some atoms on the top layer of HOPG protrude out of the base plane, and the graphite lattice of these protrusions is still intact but is strained and expanded. With further potential cycling, some protrusions coalesced and some grew larger, and an anomalous superperiodic feature was observed (spacing 90 Angstrom with a rotation 30 degrees relative to atomic corrugations) which superimposed on the atomic corrugation of HOPG. On the topmost of these protrusions, some atoms form oxides and others are still resolved by the ECSTM image. With potential cycling between -0.1 V and + 2.0 V vs. Ag/AgCl (sat. KCl), damage to freshly cleaved HOPG surface is more serious and fast, some ridges are observed, the atomic structure of the HOPG surface is partially and then completely damaged due to the formation of oxide. We also found that anodic oxidation occurred nonuniformly on the surface of HOPG near defects during potential cycling.

大西洋庸鲽Hippoglossus hippoglossus和大西洋鲑Salmo salar配子质量研究

种质问题是养殖健康发展的基础。在鱼类养殖中，卵子和精子的质量直接关系到受精、胚胎发育，仔稚鱼发育以及幼鱼生长等一系列过程。本论文针对大西洋庸鲽和大西洋鲑的配子质量进行研究。研究内容涉及大西洋庸鲽精子冷冻保存方法；促性腺激素释放激素类似物（GnRHa）使用对其精子冷冻保存效果、以及脂肪酸组成的影响；野生和驯养大西洋鲑卵子在脂肪酸、类胡萝卜素、矿物盐方面的差异比较。 精子冷冻保存通过提高对精子的利用效率，进而对于种质改良，推进鱼类养殖科研和生产具有重要意义。本实验建立了大西洋庸鲽精子大容量冷冻保存方法。八种抗冻剂冷冻保存实验结果表明：10% 及15% DMSO配以 HBSS 或KS 的抗冻剂组合冷冻保存效果最佳，4 mL体积冷冻保存可获得与1.6 mL同样的保存效果。 在繁殖季节后期注射GnRHa激素缓释剂，可获得质量稳定的大西洋庸鲽精液，将激素注射方法与精子冷冻保存方法相结合对于提高雄鱼利用率，扩大生产规模具有重要实用价值。本项研究分三个时间采集注射GnRHa激素后的雄鱼精子以及同期未注射激素的雄鱼精子，对所有精子样品使用同样的方法进行冷冻保存，检测冷冻保存后解冻精子的受精率与活力。结果表明，激素注射与否对于冷冻保存后精子的受精率和活力无显著影响，两类冷冻精液均达到鲜精水平。实验结果还表明，注射激素14天后的精子的密度显著的降低。说明GnRHa激素的使用可以显著降低精子密度，但不会影响精子的冷冻保存效果。 本相研究同时对注射GnRHa 缓释激素和未注射GnRHa 缓释激素的大西洋庸鲽精液脂肪酸成分进行分析，以检测该激素使用对精子生化组分的影响。结果表明激素的使用对在DHA (22:6n-3,二十二碳六烯酸)、EPA(20:5n-3,二十碳五烯酸)、AA(20:4n-6，花生四烯酸)等重要脂肪酸，不饱和脂肪酸、饱和脂肪酸以及n-3、n-6等重要种类的脂肪酸总量及其比例没有显著影响。精液脂肪酸中DHA含量最高，约占25%；PUFA约为44%。 作为世界性的重要养殖品种，野生和驯养大西洋鲑在形态、生化组成以及遗传 等方面表现出的差异被广泛关注。本论文，对野生和驯养大西洋鲑受精卵关键生化成分进行分析，通过与野生受精卵比较阐明驯养受精卵的质量状况，为亲鱼营养需求提供指导依据。本实验中野生配子和驯养配子的受精率没有显著差异，但重要脂肪酸组成、类胡萝卜素以及矿物盐含量都存在多方面显著差异。两类受精卵脂肪酸中含量最高的依次为18:1n-9（油酸）、DHA（二十二碳六烯酸）、16:0（棕榈酸）、EPA（二十碳五烯酸）。野生受精卵的单不饱和脂肪酸总量显著高于驯养受精卵，而多不饱和脂肪酸（PUFA）比例显著低于驯养的受精卵。在主要必需不饱和脂肪酸（EFA）中，DHA和EPA在野生受精卵中的比例高于驯养受精卵，AA（花生四烯酸）低于驯养受精卵。野生受精卵虾青素（Ax）的含量低于驯养受精卵而鸡油菌素（Cx）含量高于驯养受精卵。野生受精卵中多种矿物盐的含量（铝、铜、铁、硒和锌）含量显著高于驯养的受精卵。差别最大的为铜。诸多方面的差异表明，野生亲鱼与驯养亲鱼产出的卵子确实存在显著差异，因此关注亲鱼的营养极为重要。

马先蒿属6个种的核型与进化研究

分析和报道了马先蒿属（Pedicularis Linn.）分布于青藏高原东北部６个特有种的核型，并根据核型及其有关参数，分析和比较了该６种马先蒿核型的不对称性和相对进化程度。６个种的体细胞染色体数目都是２ｎ＝１６。核型分别为：绵德马先蒿P.pilostachya Maxim.，核型公式Ｋ（２ｎ）＝１６＝４ｍ＋１２ｓｍ，染色体相对长度组成２Ｌ＋６Ｍ２＋６Ｍ１＋２Ｓ，核型不对称系数Ａｓ·Ｋ＝６５．２９％，属于２Ａ型；青海马先蒿P.przewalskii Maxim.，Ｋ（２ｎ）＝１６＝８ｍ（ＳＡＴ）＋４ｓｍ＋２ｓ＋２ｔ，２Ｌ＋８Ｍ２＋２Ｍ１＋４Ｓ，Ａｓ·Ｋ＝６５．０２％，２Ｂ型；华马先蒿P.oederi Vahl.var.sinensis(Maxim.)Hurus.，K(2n)=16=12m+4sm，2L+4M2+8M1+2 S，As·K=59.89%，2B型；粗野马先蒿P.rudis Maxim.，K(2n)=16=4m+10sm+2st，4L+4M2+4M1+2 S，As·K=68.10%，2B型；甘肃马先蒿P.kansuensis Maxim. Subsp. kansuensis，K(2n)=16=6m+6sm+2st+2t，2L+6M2+6M1+2 S，As·K=68.92%，2A型；藓生马先蒿P.muscicola Maxim. K(2n)=16=8m(SAT)+8sm，2L=8M2+4M1+2S，As·K=62.64%，2B型。根据这6个种的核型和已有资料，认为该属的染色体基数x=8，极少数种有多倍体。通过对以上6种核型及进化程度的比较，该属核型变异较大，以中部着丝粒染色体为组成基础（较原始的种类，如华马先蒿和绵穗马先蒿），端部或近端部着丝粒染色体存在与否与该属内种的进化程度有关。核型不对称性所表示的进化程度似乎与花冠的演化有联系。

工业机器人离线编程仿真平台的研究与实现

现代计算机软硬件技术、计算机图形技术高速发展，以及数字仿真技术的广泛应用，为工业机器人离线编程技术的实际应用提供了有利条件。同时，现代生产的高效率、柔性化需求也促使了工业机器人离线编程软件产品的产生。机器人离线编程系统，是利用计算机图形学技术，建立起机器人及其工作环境的模型，利用机器人语言及相关算法，通过对图形的控制和操作在离线的情况下进行轨迹规划。离线编程技术具有传统的在线示教技术无法比拟的优势，比如：可减少停机时间、可提前验证作业程序，进行复杂的轨迹规划等。 国外的机器人离线编程软件功能已经很强大，但是只是针对特有的机器人，还不能做到像办公软件那样通用化。新松机器人公司是国内为数不多的具有自主开发工业机器人能力的公司之一，已成功开发了多款工业机器人产品，为开发自己的离线编程软件提供了客观条件，也提出了客观需求。以此为背景，本文按照软件工程的设计思想，设计了离线编程软件的框架，详细阐述了各个模块的设计原理、运行流程，对涉及到的关键技术问题，从理论、实践两个方面做了较为详细的介绍。最后，针对各个功能做了验证工作。离线编程软件系统，首先需要一个虚拟的3D仿真环境，通过该虚拟仿真环境，显示机器人的运动效果，同时为作业编程点的获取提供可视化的环境。为了提高虚拟仿真的真实程度，需要实现碰撞检测功能，并且精度和速度都要满足要求。为了便于操纵虚拟机器人，需要一个模拟示教盒的软件，以及虚拟控制器软件。为了实现多个软件之间的协作，需要传递控制流与数据流数据。 本文主要解决了整个离线编程软件系统开发过程中遇到的下列问题： (1)3D图形仿真环境的建立。本设计采用了OpenGL作为底层的图形API，并对图形显示模块做了封装，提供一组简单、方便的接口。 (2)数据结构的定义和资源管理。涉及到图形资源、抽象的仿真对象资源。为了实现多个类型的机器人能在同一仿真环境下运行，需要建立一个机器人类型库，采用了基于“抽象工厂设计”这种设计模式解决这个问题。 (3)基于3D空间的碰撞检测技术。主要采用了基于AABB包围盒和分离轴检测的技术(SAT)，实现两级计算，先粗后精。 (4)仿真环境和实际环境之间的工件标定技术。 (5)虚拟作业的建立。包括根据矩阵方法用鼠标选取操作来获取示教点，设计虚拟示教盒软件，生成作业文件。 (6)多个软件之间的通信及协议制定。