isabelle - thf 経由でオブジェクト ロジックを作成する方法

Question

Isabelle で thf 経由でオブジェクト ロジックを作成するにはどうすればよいですか?

ドキュメントでオブジェクトロジックを作成することについて私が見つけたのは、

2.3 Example: First-Order Logic

Isabelle/Isar リファレンス マニュアルに記載されています。

オブジェクト ロジックと、特に thf の使用について他に何を読むべきですか?

THF は、こちらの論文のように高次形式で型付けされます

Answer 1

簡単に言えば、現在はできません。

Isabelle には、THF のみを介してオブジェクト ロジックを定義する機能はありません。あなたが引用した例のように、オブジェクトロジックはまだPureに基づいて定義されています。