姓名：应明生

职称：教授

邮件：yingmsh@tsinghua.edu.cn

教育背景

大学专科 (数学), 江西师范学院抚州分院, 中国, 1981.

社会兼职

Artificial Intelligence Journal: 编委 (2008-).

研究领域

量子计算

程序设计语言的语义学, 人工智能中的逻辑

研究概况

1. 进程代数中的拓扑：进程代数是并发系统最成功的模型之一，其中的一个核心概念是互模拟，但它不能描述并发系统的近似行为。为了解决这个问题，我提出了进程代数中的一种拓扑理论，用于描述并发系统的近似正确性与进化过程。

2. 量子程序的Floyd-Hoare逻辑：Floyd-Hoare逻辑是经典程序公理语义学与程序正确性验证的基础。作为未来量子计算机程序设计方法学的逻辑基础，我最近为量子程序建立了包括部分正确性与完全正确性的Floyd-Hoare型逻辑，特别是证明了其（相对）完备性，其证明与经典情形不同，需要引入新的技巧，特别是分析数学的工具。

奖励与荣誉

国家自然科学二等奖——非经典计算的形式化模型与逻辑基础 (2008);

教育部自然科学一等奖——面向复杂特征的形式化方法及其逻辑基础 (2004);

中国青年科技奖 (1994).

学术成果

[1] M. S. Ying, Quantum computation, quantum theory and AI (Invited Field Review), Artificial Intelligence, 174(2010)162-176.

[2] H. Zhang and M. S. Ying, Decidable fragments of first-order language under stable model semantics and circumscription, Proc. of the 24th AAAI Conference on Artificial Intelligence (AAAI-10), 2010.

[3] W. M. Liu, X. T. Zhang, S. J. Li and M. S. Ying, Reasoning about cardinal directions between extended objects, Artificial Intelligence, (In Press, Available online 15 June 2010).

[4] M. S. Ying, R. Y. Duan, Y. Feng and Z. F. Ji, Predicate transformer semantics of quantum programs (Invited Chapter), in S. Gay and I. Mackie (eds.), Semantic Techniques in Quantum Computation, Cambridge University Press, 2010, Cambridge, pp.311-360.

[5] M. S. Ying and Y. Feng, An algebraic language for distributed quantum computing, IEEE Transactions on Computers, 58(2009)728-743.

[6] M. S. Ying, Y. Feng, R. Y. Duan and Z. F. Ji, An algebra of quantum processes, ACM Transactions on Computational Logic, 10(2009) art. no. 19.

[7] R. Y. Duan, Y. Feng, X. Yu and M. S. Ying, Distinguishability of quantum states by separable operations, IEEE Transactions on Information Theory, 55(2009)1320-1330.

[8] R. Y. Duan, Y. Feng and M. S. Ying, Perfect distinguishability of quantum operations, Physical Review Letters, 103(2009) art. no. 210501.

[9] Z. F. Ji, G. M. Wang, R. Y. Duan, Y. Feng and M. S. Ying, Parameter estimation of quantum channels, IEEE Transactions on Information Theory, 54(2008)5172-5185.

[10] R. Y. Duan, Y. Feng and M. S. Ying, Local distinguishability of multipartite unitary operations, Physical Review Letters, 100(2008) art. No. 020503.

[11] S. J. Li and M. S. Ying, Soft constraint abstraction based on semiring homomorphism, Theoretical Computer Science, 403(2008)192-201.

[12] X. T. Zhang, W. M. Liu, S. J. Li and M. S. Ying, Reasoning with cardinal directions: An efficient algorithm, in: Proc. of the 23rd AAAI Conference on Artificial Intelligence (AAAI-08), 2008, pp. 387-392.

[13] M. S. Ying, Quantum logic and automata theory (Invited Chapter), in: D. Gabbay, D. Lehmann and K. Engesser (eds), Handbook of Quantum Logic and Quantum Structures, Elsevier, 2007, Amsterdam, pp.619-754.

[14] Y. Feng, R. Y. Duan, Z. F. Ji and M. S. Ying, Proof rules for correctness of quantum programs, Theoretical Computer Science, 386(2007)151-166.

[15] Y. Feng, R. Y. Duan, Z. F. Ji and M. S. Ying, Probabilistic bisimulations for quantum processes, Information and Computation, 104(2007)152-158.

[16] R. Y. Duan, Y. Feng and M. S. Ying, Entanglement is not necessary for perfect discrimination between unitary operations, Physical Review Letters, 98(10)(2007), art. No. 100503.

[17] L. R. Xia, J. Lang and M. S. Ying, Strongly decomposable voting rules on multi-attribute domains, in: Proceedings, 22nd National Conference on Artificial Intelligence (AAAI'07).

[18] M. S. Ying, Linguistic quantifiers modeled by Sugeno integrals, Artificial Intelligence, 170(6-7)(2006), 581-606.

[19] Z. F. Ji, Y. Feng, R. Y. Duan and M. S. Ying, Identification and distance measures of measurement apparatus, Physical Review Letters, 96(20)(2006), art. No. 200401.

[20] R. Y. Duan, Y. Feng and M. S. Ying, Partial recovery of quantum entanglement, IEEE Transactions on Information Theory, 52(7)(2006), 3080-3104.

[21] Y. Z. Cao and M. S. Ying, Similarity-based supervisory control of discrete-event systems, IEEE Transactions on Automatic Control, 51 (2)(2006), 325-330.

[22] M. S. Ying, A theory of computation based on quantum logic (I), Theoretical Computer Science, 344(2-3)(2005) 134-207.

[23] M. S. Ying, Pi-calculus with noisy channels, Acta Informatica, 41(9)(2005), 525-593.

[24] M. S. Ying, Knowledge transformation and fusion for system diagnosis, Artificial Intelligence, 163(1)(2005)1-45.

[25] Y. Feng, R. Y. Duan and M. S. Ying, Catalyst-assisted probabilistic entanglement transformations, IEEE Transactions on Information Theory, 51(3)(2005), 1090-1101.

[26] X. M. Sun, R. Y. Duan, and M. S. Ying, The existence of quantum entanglement catalysts, IEEE Transactions on Information Theory, 51(1)(2005), 75-80.

[27] S. J. Li and M. S. Ying, Generalized region calculus, Artificial Intelligence, 160(1-2)(2004), 1-34.

[28] D. W. Qiu and M. S. Ying, Characterization of quantum automata, Theoretical Computer Science, 312(2-3) (2004)479-489.

[29] M. S. Ying, Reasoning about probabilistic sequential programs in a probabilistic logic, Acta Informatica, 39(5) (2003), 318-389.

[30] S. J. Li and M. S. Ying, Region connection calculus: its models and composition table, Artificial Intelligence, 145(1-2)(2003), 121-146.

[31] M. S. Ying, Bisimulation indexes and their applications, Theoretical Computer Science, 275(1-2) (2002), 1-68.

[32] M. S. Ying, Additive models for probabilistic processes, Theoretical Computer Science, 275(1-2) (2002), 481-519.

[33] M. S. Ying and H. Q. Wang, A lattice-theoretical model of consequences, conjectures and hypotheses, Artificial Intelligence, 139(2) (2002), 253-267.

[34] M. S. Ying, Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs (Research Monograph), Springer-Verlag, New York, February 2001.

[35] M. S. Ying, M. Wirsing, Recursive equations in higher-order process calculi, Theoretical Computer Science, 266(1-2) (2001), 389-352.

[36] M. S. Ying, Weak confluence and -inertness, Theoretical Computer Science, 238(1-2)( 2000), 465-475.

[37] L. Biacino, G. Gerla and M. S. Ying, Approximate reasoning based on similarity, Mathematical Logic Quarterly, 46(1)(2000), 77-86.

[38] M. S. Ying, A shorter proof to uniqueness of solutions of equations, Theoretical Computer Science, 216(1-2) (1999), 395-397.

[39] M. S. Ying, When is the ideal completion of abstract basis algebraic, Theoretical Computer Science, 159(2) (1996), 355-356.

[40] M. S. Ying, A logic for approximate reasoning, The Journal of Symbolic Logic, 59(3)(1994), 830-837.

[41] M. S. Ying, The fundamental theorem of ultraproduct in Pavelka's logic, Zeitschr. f. math. Logik und Grundlagen d. Math., 38(3)(1992), 197-201.

[42] M. S. Ying, Compactness, the Lowenheim-Skolem property and the direct product of lattices of truth values, Zeitschr. f. math. Logik und Grundlagen d. Math., 38(5-6)(1992), 521-524.

[43] M. S. Ying, Deduction theorem for many-valued inference, Zeitschr. f. math. Logik und Grundlagen d. Math., 37(6)(1991), 533-537.

[44] M. S. Ying, On a class of non-causal triangle functions, Mathematical Proceedings of Cambridge Philosophical Society, 106(3)(1989), 467-469.