We introduce our implementation in HOL Light of a prototype of a general theorem prover for normal modal logics. In the present work, we start by considering G\"odel-L\"ob provability logic (GL). The methodology consists of a shallow embedding of a labelled sequent calculus for GL whose validity relies on our formalised proof in HOL Light of modal completeness for GL w.r.t. possible world semantics, that we present in the first part of the present work. Our theorem prover for GL is thus implemented as a tactic of HOL Light that formalises the proof search in the corresponding labelled sequent calculus, and works as a decision algorithm for that logic: if the algorithm positively terminates, the tactic succeeds in producing a HOL Light theorem stating that the input formula is a theorem of GL; if the algorithm negatively terminates, the tactic extracts a model falsifying the input formula. We discuss our code for the formal proof of modal completeness, and the design of our proof search algorithm. Furthermore some examples of both interactive and automated use of the latter are shown.

翻译：我们以 HOL Light 模式验证器原型实施正常模式逻辑。 在目前的工作中, 我们首先考虑 G\ “ odel- L\” “ 可见逻辑 ” (GL) 。 方法包括将GL 标注的序列计算法(序列计算法)的浅嵌入为GL 。 该计算法的正确性依赖于我们在GL w.r.t. 可能的世界语义中展示的通用理论验证原型的正规证明。 因此, 我们的GL 理论验证法是作为HOL Light 的一种策略实施的, 它将相应标注的序列计算法正式化为证据搜索法, 并用作该逻辑的判定算法: 如果算法正终止, 策略成功生成了 HOL Light 标语, 说明输入公式是GL 的标语; 如果算法以负效果终止, 我们的策略选取了输入公式的模型。 我们讨论的代码, 以正式证明方式证明系统完整性, 以及我们的证据搜索算法的设计是自动的范例。