COQ10B在食管鳞癌中的表达及其调控Snail表达促进食管鳞癌细胞增殖与侵袭

目的:探讨COQ10B对食管鳞癌细胞增殖、侵袭能力的影响及可能的分子机制。方法:通过TIMER2.0数据库分析COQ10B基因在各种肿瘤和相邻正常组织之间的表达水平。免疫组织化学检测COQ10B在食管鳞癌组织中的表达水平并进行临床病理特征分析及生存分析;利用慢病毒构建COQ10B敲减稳转株及Snail过表达稳转株,qRT-PCR和Western blot方法检测转染效率。MTT法、Celigo细胞计数及Transwell侵袭小室检测COQ10B对KYSE150细胞系增殖和侵袭能力的影响。通过GEPIA2数据库分析COQ10B表达水平与Snail的相关性;Western blot检测敲减COQ10B对Snail蛋白表达的影响。通过拯救实验分析COQ10B是否通过正调控Snail促进KYSE150细胞系增殖和侵袭能力。结果:COQ10B在ESCC组织及细胞系中均为高表达水平,且表达水平与临床病理特征病理分级相关。COQ10B与ESCC患者预后相关,高表达COQ10B的ESCC患者预后明显较差,且发现性别、肿瘤TNM分期是影响ESCC预后的独立危险因素。敲减COQ10B可降低ESCC细胞增殖及侵袭能力。COQ10B表达水平与Snail呈正相关,并通过正调控Snail促进KYSE150细胞系增殖和侵袭能力。结论:COQ10B通过正向调控Snail基因表达促进食管鳞癌增殖与侵袭。

IGF1、CoQ10、MT联合添加缓解热应激对牛IVF囊胚的影响

旨在探明胰岛素样生长因子1(insulin-like growth factors 1,IGF1)、辅酶Q10(coenzyme Q10,CoQ10)及褪黑素(melatonin, MT)联合添加对牛卵母细胞和胚胎发育以及热应激囊胚的影响。本研究于屠宰场采集牛离体卵巢,于实验室抽取卵丘卵母细胞复合体(cumulus-oocyte complexes, COCs),在牛卵母细胞体外成熟(in vitro maturation, IVM)液及牛胚胎体外培养(in vitro culture, IVC)液中添加IGF1、CoQ10及MT,检测各添加方式对牛卵母细胞发育能力、牛卵母细胞活性氧(reactive oxygen species, ROS)水平及线粒体膜电位(mitochondrial membrane potential,ΔΨm)的影响;在囊胚期施加41℃热应激,检测热应激及联合添加对牛IVF囊胚发育能力及凋亡水平的影响,并利用qRT-PCR检测囊胚中胚胎质量相关基因mRNA表达水平。各组试验均重复3次。结果表明,与未添加组(CT-0组)相比,联合添加IGF1、CoQ10及MT组(ICM组)卵母细胞成熟率((90.40±2.06)%vs.(65.41±0.63)%)、卵裂率((93.33±1.96)%vs.(59.77±2.93)%)及囊胚率((51.43±5.34)%vs.(26.92±3.24)%)均显著提高(P<0.05);ICM组牛卵母细胞ROS水平显著降低;ΔΨm显著提高(P<0.05)。与热应激组(HS组)相比,联合添加IGF1、CoQ10及MT(ICM+HS组)显著提高了囊胚扩张率((62.00±2.97)%vs.(30.77±8.66)%,P<0.05),抑制了热应激囊胚细胞凋亡,并提高了IGFBP3、ATP1A1、DSC2及IFNT2的mRNA表达水平(P<0.05)。综上表明,联合添加IGF1、CoQ10及MT有效提高牛卵母细胞发育能力,降低ROS水平,提高ΔΨm。热应激降低牛囊胚扩张率,促进牛囊胚细胞凋亡,影响囊胚质量,而联合添加IGF1、CoQ10及MT缓解了热应激损伤。

基于MK的实数公理系统相容性和范畴性的Coq形式化

数学定理机器证明是人工智能基础理论的深刻体现.实数理论是数学分析的基础,实数公理系统是建立实数理论的重要方法.Morse-Kelley公理化集合论(MK)作为现代数学的基础,也为实数构建提供了严谨的数学框架和工具.本文使用定理证明器Coq,基于MK对实数公理系统进行了深入探索.在优化了MK形式化代码的基础上,形式化构建了完整的实数公理系统,并通过形式化Landau《分析基础》中的实数模型,证明其相对于MK相容,此外,还形式化证明了实数公理系统所有模型在同构意义下是唯一的,验证了实数公理系统的范畴性.本文全部定理无例外地给出Coq的机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.该系统可方便地应用于拓扑学和代数学理论的形式化构建.谨以此文庆祝我国著名控制系统专家秦化淑研究员九十华诞!

滩羊FGF5、COQ9基因多态性及其与生长性状的关联分析

为探索滩羊成纤维细胞生长因子5(fibroblast growth factor, FGF5)和辅酶Q9(coenzyme Q9,COQ9)基因的多态性及其与生长性状的关联性,运用分子标记辅助育种方法,为提高滩羊的生长性状提供理论依据。针对前期研究中筛选出的位点采用SNP分型技术对107只滩羊进行FGF5和COQ9基因多态性检测,并与初生重、二毛期(35日龄)、6月龄和12月龄体重进行关联分析。结果表明,通过与绵羊参考基因组(GCF_000298735.2_Oar_v4.0)比对,在滩羊FGF5基因上筛选出2个SNPs位点,分别为g.94540629T>G和g.94540642T>C,其中g.94540629T>G位点产生TT、GT和GG共3种基因型,g.94540642T>C位点产生TT、TC和CC共3种基因型;在COQ9基因上筛选出3个SNP位点,分别为g.94503480A>G、g.24807700A>G和g.24812228T>C,其中g.94503480A>G位点产生AA、AG、GG共3种基因型,g.24807700A>G位点产生AA、AG、GG共3种基因型,g.24812228T>C位点产生TT、TC和CC共3种基因型。基因多态性分析表明,5个SNPs位点属于高度多态,且在滩羊群体处于Hardy-Weinberg平衡状态(P>0.05);关联分析结果显示,FGF5基因g.94540642T>C位点C/T基因型12月体重显著大于其他基因型(P<0.05),COQ9基因g.24807700A>G位点GG基因型12月体重显著大于其他基因型(P<0.05),g.24812228T>C位点C/C基因型12月体重显著大于其他基因型(P<0.05),由此可知,3个SNP位点对滩羊12月龄体重有显著影响;COQ9基因g.24812228T>C和g.24807700A>G位点在滩羊群体处于强连锁不平衡,FGF5基因g.94540629T>G和g.94540642T>C位点在滩羊群体处于强连锁不平衡,COQ9基因g.94503480A>G、g.24807700A>G和g.24812228T>C位点和基因型组合A/GA/AT/T与A/GA/GT/C在出生重、6月体重和12月体重显著高于其他组合基因型(P<0.05)。FGF5和COQ9基因多态性与滩羊生长性状显著相关,FGF5和COQ9基因可作为滩羊生长性状选育的候选基因,可作为滩羊体重性状的分子标记,通过常规育种结合分子标记辅助选择来提高滩羊的选育效率。

基于Coq的RVWMO加载值公理形式化描述与推论证明

RISC-V内存一致性模型(RVWMO)规定了RISC-V多核系统的访存序约束,是RISC-V软硬件设计者共同遵守的重要规范,旨在为硬件设计提供灵活性的同时保证软件的易开发性。RISC-V指令集规范使用全局访存序、保留程序序以及三条公理(加载值公理、原子公理与进度保证公理)描述RVWMO。通过运用RVWMO的规则,可对多线程程序的访存序合法性进行判定,进而指导芯片设计、验证与软件开发。其中,加载值公理是最为复杂和难以运用的规则之一,是多个典型案例合法性判定的重要基础。然而,规范对于该公理的描述及案例讲解主要基于自然语言,缺乏清晰严格的形式化描述和推理过程,不利于读者理解和运用该公理。本文基于交互式定理辅助证明工具Coq,给出了RVWMO加载值公理的形式化描述以及相关引理、定理和推论的证明,对于理解运用RVWMO加载值公理和判定访存序的合法性具有重要意义。

基于Coq的逆矩阵运算的形式化

矩阵是一种在计算机科学中应用广泛的数据结构,其运算正确性具有重要意义。矩阵求逆在矩阵形式化工作当中缺乏合理且实用的形式化工作。其原因在于,工程中现有的两种常见求逆方法的形式化均存在难点。第一种是基于伴随矩阵求解方法,难点在于无法形式化地表示n*n矩阵的子矩阵,导致构建余子式组成的矩阵十分困难,因此难以实现伴随矩阵求解逆矩阵形式化;第二种称作高斯约旦初等变换求解法,难点在于构造初等矩阵及其操作函数。若使用Coq归纳结构设计操作函数,即采用行优先填充二维表的思想,将舍弃列维度对二维表的描述信息,使得操作函数分支过多,需要设计复杂的归纳结构,导致后续形式化验证无法进行。文中提出了基于记录的矩阵函数构建法,使用行列两种维度同时描述矩阵,使得构造并证明初等矩阵成为可能,在此基础上实现了在Coq系统中基于高斯约旦消元法的矩阵求逆的形式化工作。以一种代价更小且时间复杂度更低的方式,实现了首个形式化验证下的软件逆矩阵函数库。

COQ8B相关肾病患儿的基因型和表型特点及肾移植预后分析

目的总结辅酶Q8B(coenzyme Q8B,COQ8B)相关肾病患儿的基因型和表型特点以及肾移植相关预后,为COQ8B相关肾病患儿的诊疗提供参考。方法回顾性分析中山大学附属第一医院2017—2022年间接受肾移植手术的COQ8B相关肾病患儿的基因型、表型和预后相关信息,患者的纳入标准为接受了下一代测序技术(next-generation sequencing,NGS)检测并且携带COQ8B的致病突变。结果18例获得COQ8B相关肾病分子诊断的患儿被纳入研究,其中13例患儿携带COQ8B的复合杂合突变,5例患儿携带COQ8B的纯合突变,c.748G>C是本地区最常见的突变位点。患儿的平均发病年龄为(9.09±2.57)岁,到达终末期肾病的平均年龄为(9.72±2.84)岁。18例患儿中有15例表现为孤立的肾病,有3例患儿出现了肾外器官受累。患儿术后的平均随访时间为31.7个月,随访期间内仅有1例发生排斥反应,无原发病复发和移植肾失功等事件发生。患儿的生长发育状况在术后也得到了一定改善,术前的中位年龄别身高z评分(height-for-age z-score,HAZ)为-1.47(-1.95,-0.9),术后1年的中位HAZ为-1.25(-1.77,-0.7),术后第2年的中位HAZ为-0.91(-1.24,-0.34)。结论COQ8B相关肾病多表现为孤立的肾病综合征,较少出现肾外器官的病变,对于已经处于晚期肾病阶段的患儿,肾移植是一种安全有效的治疗方式。

针对教学场景的ZFC集合论Coq形式化

离散数学是计算机类专业的基础课程之一,命题逻辑、一阶逻辑与公理集合论是其重要组成部分.教学实践表明,初学者准确理解语法、语义、推理系统等抽象概念是有一定难度的.近年来,已有一些学者开始在教学中引入交互式定理证明工具,以帮助学生构造形式化证明,更透彻地理解逻辑系统.然而,现有的定理证明器有较高上手门槛,直接使用会增加学生的学习负担.鉴于此,在Coq中开发了针对教学场景的ZFC公理集合论证明器.首先,形式化了一阶逻辑推理系统和ZFC公理集合论;之后,开发了数条自动化推理规则证明策略.学生可以在与教科书风格相同的简洁证明环境中使用自动化证明策略完成定理的形式化证明.该工具被用在了大一新生离散数学课程的教学中,没有定理证明经验的学生使用该工具可以快速完成数学归纳法和皮亚诺算术系统等定理的形式化证明,验证了该工具的实际效果.

微内核操作系统互斥量模块功能正确性的形式化验证

操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误,因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中,互斥量可协调多任务对资源的访问,是一种常用的任务同步方式,其功能正确性对于保障多任务应用的正确性十分关键.基于定理证明方法,在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模,给出其接口函数的形式化规范,并实现这些接口函数的功能正确性验证.

舰载机弹药保障作业调度的形式化建模与验证

航母舰载机弹药保障作业的智能规划作为一种高效能航保作业调度方法,是助推航母工程先进技术建设发展的重要途径之一.高安全攸关属性下作业规划方案的正确性保证已经逐渐成为制约其实际应用部署安全的关键技术瓶颈.针对方案正确性验证中存在的弹药保障系统难建模、作业执行行为难描述、形式验证工具难实现等挑战,基于分离逻辑的思想,提出一种弹药保障系统的行为模型,并利用定理证明器Coq对作业规划方案进行形式化验证.首先提出一个符合弹药保障作业特征的序列化双层资源堆模型;基于该模型,构造一套可用于描述作业执行行为的建模语言及其操作语义;最后在Coq中实现一种证明辅助工具.通过几个典型弹药保障作业规划方案的交互式证明实例,验证工具的可用性与工程实用性.

几种营养物质对烟草细胞生长和CoQ_(10)含量的影响

研究了蔗糖、KH2PO4、NH+4/NO3比对烟草细胞生长和CoQ10含量的影响,结果表明,当蔗糖浓度为30g/L时,CoQ10总量最高,此时细胞产量、CoQ10含量和总量分别为198g/L、4147μg/g(dwt)、8212μg/L。在上述蔗糖浓度下,当KH2PO4起始浓度为340mg/L、NH+4/NO-3为12时,细胞产量、CoQ10含量和总量分别最高,高于此比例时有利于CoQ10形成,但不利于细胞生长。

烟草细胞悬浮培养生产CoQ_(10)的条件研究

采用细胞悬浮培养的方法,以烟草(NicotianatobacumL)细胞为材料,研究了不同温度、不同pH值、愈伤组织不同接种年龄和接种量对烟草细胞生长和CoQ10形成的影响.结果表明,在16～32℃间细胞能生长形成CoQ10,但在16～28℃范围内,细胞生物量随温度升高递增;在24～32℃范围内,CoQ10含量随温度上升而下降.在pH值为5～7 5条件下细胞能生长和形成CoQ10,当pH值为5 8时细胞干重和CoQ10含量最大.悬浮培养接种的"种子"年龄为7d左右时细胞干重及CoQ10含量均最大;接种量与培养基的质量分数比为1∶7 5时,较适合细胞生长和CoQ10的合成.

运动性疲劳的线粒体膜分子机理研究V:线粒体CoQ和质子循环共同参与ROS循环——运动模型中的证据

目的 :以运动、外源性补充辅酶Q (coenzymeQ ,CoQ)以及运动合并补充CoQ作为干预手段 ,观察线粒体CoQ结合含量、质子跨膜势能与活性氧产生之间的相互关系 ,进一步探讨运动性内源活性氧生成和代谢的线粒体膜分子机制。方法 :雄性SD大鼠 36只 ,随机分为 :(1)安静对照组 (R ,n =6 ) ;(2 )运动中对照组 (Em ,n =6 ) ;(3)力竭对照组 (Ei,n =6 ) ;(4 )安静补药组 (QR ,n=6 ) ;(5 )运动中补药组 (Qm ,n =6 ) ;(6 )力竭补药组 (Qi ,n =6 )。采用三级递增负荷力竭运动模型 ,测定心肌线粒体CoQ9及CoQ10 结合含量、ROS产生速率以及线粒体膜质子泵出与电子传递比值(H+/ 2e)。结果 :(1)Em和Qm组心肌线粒体ROS产生、H+/ 2e和CoQ结合含量分别比R和QR组显著增高 ,并且 ,Qm组三项指标显著高于Em组。 (2 )相关分析表明 ,CoQ结合含量分别与H+/ 2e和ROS产生速率呈线性正相关。结论 :以外源性补充CoQ10 和 /或运动应激作为干预手段时 ,心肌线粒体CoQ含量升高导致建立高质子跨膜势能 ,并进而增加活性氧生成 ,进一步支持“活性氧循环”

培养条件对烟草细胞生长和CoQ_(10)含量的影响

以红花大金元品种的烟草为材料 ,采用细胞悬浮培养方法 ,对影响烟草生长和CoQ10 含量的细胞培养条件 :pH、温度、接种量、摇床转速及装液量等进行了研究 结果表明 :烟草细胞在培养基原始pH 4 0～ 8 0下均能生长 ,但在pH 6 0时细胞生长最好 ,CoQ10 含量最高 ;接种量仅能影响细胞培养周期 ,而不影响CoQ10 含量 ,接种量增加可缩短细胞生长的迟滞期 ;在 1 6～ 32℃间 ,温度升高有利于CoQ10 的形成 ,但超过 2 8℃则不利于烟草细胞的生长 ,CoQ10总量并不增加 ;摇床转速和装液量对细胞生长和CoQ10 形成的影响主要是其造成的剪切力和溶氧量的变化 ,摇床转速在 1 0 0～ 1 5 0r/min范围内有利于烟草细胞生长和CoQ10 形成 在 1 0 0r/min转速下 ,细胞干质量和CoQ10 含量最高 ,此时 (装液量为 1 0 0mL瓶的 1 /4 )的Kd 值为 1 74pmol(mL·min·Pa)

基于Coq的软件安全性验证

针对数组越界、空指针应用和缓冲区溢出三类威胁软件安全的不规范操作,提出了一种基于Coq验证上述三类操作的形式化方法。首先编写三类安全问题的程序实例,并采用形式化方法进行标注;其次运用Frama-C和Why工具对标注程序进行解析,生成需要证明的定理;最后基于Coq集成开发环境证明定理,实现安全问题的验证。结果表明,该方法有效验证了软件安全中的三类问题,为形式化方法在软件安全性验证方面的应用奠定了基础。

一株产CoQ_(10)的红假单胞菌的研究

从滇池分离到一株革兰氏阴性杆菌 ,于光照厌氧及黑暗好氧条件下生长良好 ,活细胞在 870、80 3 nm处有吸收峰 ,具平行片层状的光合内膜系统 ,可归属于红假单胞菌属 (Rhodopseudomonas) ;该菌体中提取分离得到的黄色结晶品 ,经 Craven试验、高效薄层层析、高效液相色谱、紫外光谱、红外光谱、核磁共振及质谱证实 ,为 Co Q1

CoQ_(10)生物合成限速酶及其编码基因对布莱凯特黑牛品种培育的实践意义

辅酶Q10(CoQ10)作为人体线粒体呼吸链中的递氢体具有较高的学术研究及应用价值。由ubiA/coq2基因编码的对羟苯甲酸聚异戊二烯焦磷酸转移酶是原核和真核生物CoQ生物合成途径的限速步骤,因此对该酶及其编码基因的研究显得尤为重要。对该酶及其编码基因的研究成果和现状进行综述和展望,旨在为布莱凯特黑牛品种培育的实践研究提供理论指导意义。

微生物CoQ合成途径及CoQ_(10)生产菌株的分子生物学改造

CoQ10具有呼吸链电子传递者、抗氧化性、调控基因表达等多种生理生化功能,目前不仅用作药物也用作食品添加剂。微生物发酵法是目前生产CoQ10最有效的方法。就有关微生物CoQ合成途径及基于CoQ合成途径的CoQ10生产菌株分子生物学改造的策略与研究进展进行了综述和展望。

CoQ10软胶囊在Beagle犬体内的相对生物利用度评价

目的:比较在 Beagle 犬体内3种辅酶 Q_(10)(CoQ_(10))制剂的相对生物利用度。方法:采用三制剂三周期(3×3拉丁方)自身对照交叉多剂量口服给药方式,周期间清洗1周。用高效液相色谱法测定6条健康 Beagle 犬口服 CoQ_(10)软胶囊(受试制剂A)、CoQ_(10)普通胶囊(参比制剂 B)和进口 CoQ_(10)软胶囊(参比制剂 C)后不同时间点血浆中 CoQ_(10)的浓度,扣除内源性 CoQ_(10)本底,绘制血药浓度-时间曲线,计算相对生物利用度。结果:受试犬口服 CoQ_(10)60mg 的受试制剂(A)和参比制剂(B,C)后,血浆中 CoQ_(10)AUC_(0-t)(μg·h·mL^(-1))分别为69.31±40.49,62.38±59.05,104.90±64.32。与参比制剂 B 与 C 相比,受试制剂中的相对生物利用度平均为(144.07±79.48)%和(78.60±54.28)%。结论:CoQ_(10)受试制剂 A 生物利用度高于参比制剂 B 而低于参比制剂 C。

磁胁迫对烟草细胞生长和CoQ_(10)含量的影响

用0.4 T恒定磁场处理烟草细胞0.5～1.5 h后,细胞活力和存活率可受到一定的影响,但处理间差异不显著.处理0.5～1.0h的细胞分裂指数和细胞生物量显著提高,分别提高15.4%和49.6%,细胞干重分别提高18.4%和42.3%,但CoQ10的生物合成和积累受抑.处理1.5 h的细胞分裂和细胞生长受抑,但CoQ10的生物合成和积累得到促进,CoQ10含量提高25.2%.