We give a relational and a weakest precondition semantics for ``knowledge-based programs'', i.e., programs that restrict observability of variables so as to richly express changes in the knowledge of agents who can or cannot observe said variables. Based on these knowledge-based programs, we define a program-epistemic logic to model complex epistemic properties of the execution of multi-agent systems. We translate the validity of program-epistemic logic formulae into first-order validity, using our weakest precondition semantics and an ingenious book-keeping of variable assignment. We implement our translation in Haskell in a general way (i.e., independently of the programs in the logical statements), and test this novel verification method for our new program-epistemic logic on a series of well-established examples.

翻译：我们给“基于知识的方案”提供一种关系和最弱的先决条件语义,即限制变量可视性的方案,以便能或无法观察所述变量的代理方的知识发生大量变化。基于这些基于知识的方案,我们定义了一种程序-全能逻辑,以模拟执行多试剂系统的复杂认知特性。我们用我们最弱的前提条件语义和奇特的可变任务书记,将程序-全能逻辑公式的有效性转换为一等有效。我们用一般方式(即独立于逻辑语句中的程序)在哈斯凯尔进行翻译,并在一系列公认的实例中测试我们新的程序-全能逻辑的这一新型核查方法。