模态k4、d4系统的归结推理

本文将ｐ．ｅｎｊａｌｂｅｒｔ和ｌ．ｆａｒｉｎａｓｄｅｌｃｅｒｒｏ提出的模态归结推理方法推广到命题模态逻辑k4和d4系统，建立了k4逻辑的归结推理ｒk4；d4逻辑的归结推理rd4，分别证明了ｒk4和ｒd4关于k