Health records of traditional Chinese medicine contain valuable clinical inlormation which can be used for improvement of disease treatment and for medical research. In this paper, we present a practical iterative ext...Health records of traditional Chinese medicine contain valuable clinical inlormation which can be used for improvement of disease treatment and for medical research. In this paper, we present a practical iterative extraction method for extracting terms from the records. The method is based on a set of extraction rules, the Mesh, and the likelihood ratio technique, and achieved a precision rate of 88.18% and a recall rate of 94.21%.展开更多
A sequent is a pair(Г,△),which is true under an as-signment if either some formula inГis false,or some formula in △ is true.In L3-valued propositional logic,a mulisequent is a triple △|Θ|Г,which is true under a...A sequent is a pair(Г,△),which is true under an as-signment if either some formula inГis false,or some formula in △ is true.In L3-valued propositional logic,a mulisequent is a triple △|Θ|Г,which is true under an assignment if either some formula in △ has truth-value t,or some formula in Θ has truth-value m,or some formula in Г has truth-value￡.Corre-spondingly there is a sound and complete Gentzen deduction system G for multisequents which is monotonic.Dually,a CO-multisequent is a triple △:Θ:Г,which is valid if there is an assignment v in which each formula in△has truth-value≠t,each formula in Θ has truth-value≠m,and each formula in Г has truth-value≠￡.Correspondingly there is a sound and com-plete Gentzen deduction system G-for co-multisequents which is nonmonotonic.展开更多
Hoare logic is a logic used as a way of specifying semantics of programming languages, which has been extended to be a separation logic to reason about mutable heap structure. In a model M of Hoare logic, each program...Hoare logic is a logic used as a way of specifying semantics of programming languages, which has been extended to be a separation logic to reason about mutable heap structure. In a model M of Hoare logic, each program α induces an M-computable function fα M on the universe of M; and the M-recursive functions are defined on M. It will be proved that the class of all the M-computable functions fα M induced by programs is equal to the class of all the M- recursive functions. Moreover, each M-recursive function is ∑ 1 NM -definable in M, where the universal quantifier is a num- ber quantifier ranging over the standard part of a nonstandard model M.展开更多
文摘Health records of traditional Chinese medicine contain valuable clinical inlormation which can be used for improvement of disease treatment and for medical research. In this paper, we present a practical iterative extraction method for extracting terms from the records. The method is based on a set of extraction rules, the Mesh, and the likelihood ratio technique, and achieved a precision rate of 88.18% and a recall rate of 94.21%.
文摘A sequent is a pair(Г,△),which is true under an as-signment if either some formula inГis false,or some formula in △ is true.In L3-valued propositional logic,a mulisequent is a triple △|Θ|Г,which is true under an assignment if either some formula in △ has truth-value t,or some formula in Θ has truth-value m,or some formula in Г has truth-value￡.Corre-spondingly there is a sound and complete Gentzen deduction system G for multisequents which is monotonic.Dually,a CO-multisequent is a triple △:Θ:Г,which is valid if there is an assignment v in which each formula in△has truth-value≠t,each formula in Θ has truth-value≠m,and each formula in Г has truth-value≠￡.Correspondingly there is a sound and com-plete Gentzen deduction system G-for co-multisequents which is nonmonotonic.
文摘Hoare logic is a logic used as a way of specifying semantics of programming languages, which has been extended to be a separation logic to reason about mutable heap structure. In a model M of Hoare logic, each program α induces an M-computable function fα M on the universe of M; and the M-recursive functions are defined on M. It will be proved that the class of all the M-computable functions fα M induced by programs is equal to the class of all the M- recursive functions. Moreover, each M-recursive function is ∑ 1 NM -definable in M, where the universal quantifier is a num- ber quantifier ranging over the standard part of a nonstandard model M.
