论文09:58HOL中一阶模态逻辑的深与浅嵌入及自动忠实性（扩展预印本）这篇论文用Isabelle/HOL把一阶模态逻辑的深和浅嵌入都严格形式化了，还自动化证明了忠实性，做形式化逻辑或模态逻辑验证的值得看。#Isabelle/HOL#一阶模态逻辑#深嵌入#浅嵌入aarXiv cs.AI@Christoph Benzmüller, Daniel Kirchner原文稍后读已读值得跟进有用关注 Isabelle/HOL