完全宣言型ホーン ロジック(または完全宣言型プロローグ)と呼ばれるもので、いくつかの知識を形式化し、クエリを実行したいと考えています。誰かがそれを実装する方法に関するガイドラインを提供できますか? 上記のリンクからの詳細な説明を簡単に要約します。
正式な言語は、Prolog (のコア) のものです。「プログラム」は、Prolog と同様に、規則と事実のセットです (関数と変数を含み、基本的にはユーザー定義の述語のみを含みます)。
ただし、Prolog とは対照的に、論理プログラムの標準的な宣言的セマンティクスに関して健全で完全な実装、つまり最小の Herbrand モデル (帰納的に定義された基本用語のセット) を探しています。論理プログラミングの理論的研究では、これは通常研究の対象であり、たとえば、次の条件:
- マッチング ルールの公平な検索 (たとえば、Prolog の深さ優先検索は公平ではありません)。
- "発生チェック" による統一 (変数が統一された項に出現しないことを確認する)。
車輪を発明するのではなく、既存の機能に基づいて構築される簡潔な実装を探しています。私が見ているより有望な方向性の 2 つは、Prolog のメタインタープリターとして、または何らかの定理証明の一部として実装することです。これらの分野で実際的な知識を持っている人は、それを実装する方法に関するガイドラインを提供できますか? miniKanrenで簡単に実装できますか?
私の意図は、一部の知識を完全に宣言的な方法で形式化することです。このような形式化の重要な特徴は、それが (単調な) 帰納法の数学的概念に正確に対応しているため、知識とその特性を帰納的な議論で簡単に推論できることです。