论文标题
Hol Light机械化Gödel-Löb的可预订性逻辑
Mechanising Gödel-Löb provability logic in HOL Light
论文作者
论文摘要
我们介绍了Gödel-LöbProvability逻辑（GL）的元素质量，介绍了我们的实施，涵盖了健全性和完整性W.R.T.可能的世界语义，并具有GL本身定理供款的原型。我们在这里制定的策略以形式化模态完整性证明克服了由于GL的非压缩性而导致的技术困难，并且根据手头的正式语言和工具的适应性 - 乔治·布洛斯（George Boolos）在1995年的专着中给出了证明。 Our theorem prover for GL relies then on this formalisation, is implemented as a tactic of HOL Light that mimics the proof search in the labelled sequent calculus G3KGL, and works as a decision algorithm for the provability 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;如果该算法终止算法，则策略提取了一个模型，以伪造输入公式。我们讨论了我们的代码，以形式上完整性证明和我们的证明搜索算法的设计。此外，我们提出了后者的互动和自动使用的一些示例。
We introduce our implementation in HOL Light of the metatheory for Gödel-Löb provability logic (GL), covering soundness and completeness w.r.t. possible world semantics and featuring a prototype of a theorem prover for GL itself. The strategy we develop here to formalise the modal completeness proof overcomes the technical difficulty due to the non-compactness of GL and is an adaptation -- according to the formal language and tools at hand -- of the proof given in George Boolos' 1995 monograph. Our theorem prover for GL relies then on this formalisation, is implemented as a tactic of HOL Light that mimics the proof search in the labelled sequent calculus G3KGL, and works as a decision algorithm for the provability 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, we propose some examples of the latter's interactive and automated use.
