In this paper, some necessary and sufficient conditions that a finite lattice implication algebra is simple are established. Specially, it is proved that a finite lattice implication algebra L is simple if and only if...In this paper, some necessary and sufficient conditions that a finite lattice implication algebra is simple are established. Specially, it is proved that a finite lattice implication algebra L is simple if and only if （L, ≤） is a chain, if and only if there exists the unique dual atom in L. Also, it is given that a finite lattice implication algebra with order of a prime number is simple.展开更多
Two new types of lentiviral vectors expressing a reporter transgene encoding either firefly luciferase （fLuc） for bioluminescence imaging or the HSV1 thymidine kinase （HSV1-TK） for radiopharmaceutical-based imagin...Two new types of lentiviral vectors expressing a reporter transgene encoding either firefly luciferase （fLuc） for bioluminescence imaging or the HSV1 thymidine kinase （HSV1-TK） for radiopharmaceutical-based imaging were constructed to monitor human embryonic stem cell （hESC） engraftment and proliferation in live mice after trans- plantation. The constitutive expression of either transgene did not alter the properties of hESCs in the culture. We next monitored the formation of teratomas in SCID mice to test （1） whether the gene-modified hESCs maintain their developmental pluripotency, and （2） whether sustained reporter gene expression allows noninvasive, whole-body imaging of hESC derivatives in a live mouse model. We observed teratoma formation from both types of gene-modified cells as well as wild-type hESCs 2-4 months after inoculation. Using an optical imaging system, bioluminescence from the fLuc-transduced hESCs was easily detected in mice bearing teratomas long before palpable tumors could be detected. To develop a noninvasive imaging method more readily translatable to the clinic, we also utilized HSV1-TK and its specific substrate, 1-（2＇-deoxy-2＇-fluoro-β-D-arabinofuranosyl）-5-[^125I]iodouracil（[^125I]FIAU）, as a reporter/ probe pair. After systemic administration, [^125I]FIAU is phosphorylated only by the transgene-encoded HSV1-TK enzyme and retained within transduced （and transplanted） cells, allowing sensitive and quantitative imaging by single-photon emission computed tomography. Noninvasive imaging methods such as these may enable us to monitor the presence and distribution of transplanted human stem cells repetitively within live recipients over a long term through the expression of a reporter gene.展开更多
We first prove that for a finite dimensional non-semisimple Hopfalgebra H, the trivial H-module is not projective and so the almost split sequence ended with k exists. By this exact sequence, for all indecomposable H-...We first prove that for a finite dimensional non-semisimple Hopfalgebra H, the trivial H-module is not projective and so the almost split sequence ended with k exists. By this exact sequence, for all indecomposable H-module X, we can construct a special kind of exact sequence ending with it. The main aim of this paper is to determine when this special exact sequence is an almost split one. For this aim, we restrict H to be tmimodular and the square of its antipode to be an inner automorphism. As a special case, we give an application to the quantum double D（H）=（H^op）^＊∞ H） of any non-semisimple Hopf algebra.展开更多
Satisfiability modulo theories (SMT) play a key role in verification applications. A crucial SMT problem is to combine separate theory solvers for the union of theories. In previous work, the simplex method is used to...Satisfiability modulo theories (SMT) play a key role in verification applications. A crucial SMT problem is to combine separate theory solvers for the union of theories. In previous work, the simplex method is used to determine the solvability of constraint systems and the equalities implied by constraint systems are detected by a multitude of applications of the dual simplex method. We present an effective simplex tableau-based method to identify all implicit equalities such that the simplex method is harnessed to an irreducible minimum. Experimental results show that the method is feasible and effective.展开更多
基金Supported by a grant of Natural Science Foundation of Guangdong Province in China（021073）
文摘In this paper, some necessary and sufficient conditions that a finite lattice implication algebra is simple are established. Specially, it is proved that a finite lattice implication algebra L is simple if and only if （L, ≤） is a chain, if and only if there exists the unique dual atom in L. Also, it is given that a finite lattice implication algebra with order of a prime number is simple.
文摘Two new types of lentiviral vectors expressing a reporter transgene encoding either firefly luciferase （fLuc） for bioluminescence imaging or the HSV1 thymidine kinase （HSV1-TK） for radiopharmaceutical-based imaging were constructed to monitor human embryonic stem cell （hESC） engraftment and proliferation in live mice after trans- plantation. The constitutive expression of either transgene did not alter the properties of hESCs in the culture. We next monitored the formation of teratomas in SCID mice to test （1） whether the gene-modified hESCs maintain their developmental pluripotency, and （2） whether sustained reporter gene expression allows noninvasive, whole-body imaging of hESC derivatives in a live mouse model. We observed teratoma formation from both types of gene-modified cells as well as wild-type hESCs 2-4 months after inoculation. Using an optical imaging system, bioluminescence from the fLuc-transduced hESCs was easily detected in mice bearing teratomas long before palpable tumors could be detected. To develop a noninvasive imaging method more readily translatable to the clinic, we also utilized HSV1-TK and its specific substrate, 1-（2＇-deoxy-2＇-fluoro-β-D-arabinofuranosyl）-5-[^125I]iodouracil（[^125I]FIAU）, as a reporter/ probe pair. After systemic administration, [^125I]FIAU is phosphorylated only by the transgene-encoded HSV1-TK enzyme and retained within transduced （and transplanted） cells, allowing sensitive and quantitative imaging by single-photon emission computed tomography. Noninvasive imaging methods such as these may enable us to monitor the presence and distribution of transplanted human stem cells repetitively within live recipients over a long term through the expression of a reporter gene.
基金Project (No. 10371107) supported by the National Natural ScienceFoundation of China
文摘We first prove that for a finite dimensional non-semisimple Hopfalgebra H, the trivial H-module is not projective and so the almost split sequence ended with k exists. By this exact sequence, for all indecomposable H-module X, we can construct a special kind of exact sequence ending with it. The main aim of this paper is to determine when this special exact sequence is an almost split one. For this aim, we restrict H to be tmimodular and the square of its antipode to be an inner automorphism. As a special case, we give an application to the quantum double D（H）=（H^op）^＊∞ H） of any non-semisimple Hopf algebra.
基金Project supported by the National Natural Science Foundation of China (Nos 60635020 and 90718039)the National Basic Research Program (973) of China (No 2004CB719406)
文摘Satisfiability modulo theories (SMT) play a key role in verification applications. A crucial SMT problem is to combine separate theory solvers for the union of theories. In previous work, the simplex method is used to determine the solvability of constraint systems and the equalities implied by constraint systems are detected by a multitude of applications of the dual simplex method. We present an effective simplex tableau-based method to identify all implicit equalities such that the simplex method is harnessed to an irreducible minimum. Experimental results show that the method is feasible and effective.
