R C.T.Lee和C.L.Chang首先讨论了真值集为单位区间的模糊逻辑,特别是证明了一阶谓词公式在二值逻辑中的不可满足性与在这种模糊逻辑中的不可满足性是等价的,从而原始的归结原理在这种模糊逻辑中是完备的。1980年,刘叙华将[1,2]的结果推...R C.T.Lee和C.L.Chang首先讨论了真值集为单位区间的模糊逻辑,特别是证明了一阶谓词公式在二值逻辑中的不可满足性与在这种模糊逻辑中的不可满足性是等价的,从而原始的归结原理在这种模糊逻辑中是完备的。1980年,刘叙华将[1,2]的结果推广到有分界元素的有余完全分配格值逻辑,并称这种逻辑为广义模糊逻辑,容易知道,真值格有分界元素这个条件是比较苛刻的。展开更多
量子硬件设计与制造技术的飞速发展使得人们开始预言大于100个量子比特的特定用途的量子计算机有望在5～10年内实现.可以想见,到那时候,量子软件的开发将变成真正发挥这些计算机能力的关键因素.然而,由于量子信息的不可克隆性和纠缠的...量子硬件设计与制造技术的飞速发展使得人们开始预言大于100个量子比特的特定用途的量子计算机有望在5～10年内实现.可以想见,到那时候,量子软件的开发将变成真正发挥这些计算机能力的关键因素.然而,由于量子信息的不可克隆性和纠缠的非局域作用等量子特征,如何设计正确、高效的量子程序和量子通信协议将是一个富有挑战性的课题.形式化验证方法,特别是模型检测技术,已在经典软件设计和系统建模方面被证明行之有效,因此量子软件的形式化验证也开始受到越来越多的关注.从量子顺序程序验证和量子通信协议验证两方面,对近年来国内外学者,尤其对University of Technology Sydney和清华大学的研究组在该研究领域取得的一些成果进行了系统的总结.最后,对未来可能的研究方向和面临的挑战进行了简单展望.展开更多
文摘量子硬件设计与制造技术的飞速发展使得人们开始预言大于100个量子比特的特定用途的量子计算机有望在5～10年内实现.可以想见,到那时候,量子软件的开发将变成真正发挥这些计算机能力的关键因素.然而,由于量子信息的不可克隆性和纠缠的非局域作用等量子特征,如何设计正确、高效的量子程序和量子通信协议将是一个富有挑战性的课题.形式化验证方法,特别是模型检测技术,已在经典软件设计和系统建模方面被证明行之有效,因此量子软件的形式化验证也开始受到越来越多的关注.从量子顺序程序验证和量子通信协议验证两方面,对近年来国内外学者,尤其对University of Technology Sydney和清华大学的研究组在该研究领域取得的一些成果进行了系统的总结.最后,对未来可能的研究方向和面临的挑战进行了简单展望.
