摘要: “知道”逻辑是诸多学科领域共同关心的课题。近年来,从数理逻辑角度对此进行研究所得的一些成果,在计算机人工智能中有着重要的应用。本文介绍了这方面的有关问题及进展,构造了“知道”的模态逻辑的谓词演算,包括建立其形式系统(命名为W),给出它的语义解释(命名为JS),讨论W-JS的某些重要的系统特征,并通过著名的“S先生和P先生”谜题,阐述了有关“知道”的模态逻辑问题在W-JS下的形式化。