isabelle - 如何通过 thf 创建对象逻辑

Question

如何通过 thf 在 Isabelle 中创建对象逻辑？

我发现在文档中创建对象逻辑是

2.3 Example: First-Order Logic

在 Isabelle/Isar 参考手册中。

我还应该阅读关于对象逻辑和特别是使用 thf 的哪些内容？

THF 是在这里的论文中输入的高阶形式

Answer 1

简短的回答是：目前，你不能。

Isabelle 中没有工具可以仅通过 THF 定义对象逻辑。对象逻辑仍然是在 Pure 上定义的，就像您引用的示例一样。