論理フレームワーク

論理学において、論理フレームワークは、元の論理における式の証明可能性がフレームワーク型理論における型居住問題に還元されるように、高階型理論におけるシグネチャとして論理を定義（または提示）する手段を提供する。 ^{[1] [2]このアプローチは、（対話型の）}自動定理証明に効果的に使用されてきた。最初の論理フレームワークはAutomathであったが、このアイデアの名前は、より広く知られているEdinburgh Logical Framework、LFに由来している。Isabelleなどの最近の証明ツールのいくつかは、このアイデアに基づいている。^[1]直接的な埋め込みとは異なり、論理フレームワークアプローチでは、同じ型システムに多くのロジックを埋め込むことができる。^[3]

論理フレームワークは、依存型ラムダ計算による構文、規則、証明の一般的な処理に基づいています。構文は、 Per Martin-Löfのアリティ システム に似ていますが、より一般的なスタイルで処理されます。

論理フレームワークを記述するには、次のものを提供する必要があります。

1. 表現されるオブジェクトロジックのクラスの特性。
2. 適切なメタ言語。
3. オブジェクトロジックが表現されるメカニズムの特徴付け。

これを要約すると次のようになります。

「フレームワーク = 言語 + 表現」

LF 論理フレームワークの場合、メタ言語はλΠ 計算です。これは、命題を型原理として関連付けることにより、第 1 階の 極小論理に関連付けられた第 1 階の従属関数型のシステムです。λΠ 計算の主な特徴は、オブジェクト、型、種類 (または型クラス、型のファミリー) という 3 つのレベルのエンティティで構成されていることです。これは述語的であり、適切に型付けされたすべての項は強く正規化され、チャーチ-ロッサーであり、適切に型付けされているというプロパティは決定可能です。ただし、型推論は決定不可能です。

LF 論理フレームワークでは、論理は判断を型として表現するメカニズムによって表現されます。これは、1983 年のシエナ講義でペル・マルティン＝レーフがカントの判断の概念を展開したことにヒントを得ています。仮説的判断と一般判断という2 つの高階判断は、それぞれ通常の関数空間と従属関数空間に対応します。判断を型として表現する方法論では、判断は証明の型として表現されます。論理システムは、その構文、判断、ルール スキームを表す有限の定数セットに種類と型を割り当てるシグネチャによって表現されます。オブジェクト ロジックのルールと証明は、仮説的一般判断の原始的な証明と見なされます。 ${\displaystyle J\vdash K}$${\displaystyle \Lambda x\in JK(x)}$ ${\displaystyle {\mathcal {L}}}$${\displaystyle \Lambda x\in CJ(x)\vdash K}$

LF論理フレームワークの実装は、カーネギーメロン大学のTwelfシステムによって提供されています。Twelfには以下が含まれます。

• 論理プログラミングエンジン
• 論理プログラムに関するメタ理論的推論（終了性、カバレッジなど）
• 帰納的メタ論理定理証明器

• 文法の枠組み
• 改札口（シンボル）

• フランク・フェニング(2002)。 「論理フレームワーク – 簡単な紹介」。ヘルムート・シュヴィヒテンベルク、ラルフ・シュタインブリュッゲン（編）。証明とシステムの信頼性(PDF)。スプリンガー。ISBN 978-1-4020-0608-1。
• Robert Harper、Furio Honsell、Gordon Plotkin。「ロジックを定義するためのフレームワーク」。Journal of the Association for Computing Machinery、40(1):143-184、1993年。
• Arnon Avron、Furio Honsell、Ian Mason、Randy Pollack。型付きラムダ計算を使用したマシン上での形式システムの実装。Journal of Automated Reasoning、9:309-354、1992 年。
• Robert Harper。LFの等式定式化。技術レポート、エディンバラ大学、1988 年。LFCS レポート ECS-LFCS-88-67。
• Robert Harper、Donald Sannella、Andrzej Tarlecki。構造化理論のプレゼンテーションと論理表現。純粋および応用論理の年報、67(1-3):113-160、1994年。
• Samin Ishtiaq と David Pym。自然演繹の適切な分析。Journal of Logic and Computation 8、809-838、1998 年。
• Samin Ishtiaq と David Pym。依存型、束ねられた計算${\displaystyle \lambda}$の Kripke リソース モデル。Journal of Logic and Computation 12(6)、1061-1104、2002 年。
• ペル・マーティン＝レーフ「論理定数の意味と論理法則の正当化について」『北欧哲学論理学ジャーナル』1(1):11-60、1996年。
• Bengt Nordström、Kent Petersson、Jan M. Smith。Martin -Löf の型理論におけるプログラミング。オックスフォード大学出版局、1990 年。(この本は絶版ですが、無料版が提供されています。)
• デイヴィッド・ピム。-計算の証明理論に関するノート${\displaystyle \lambda \Pi }$。論理学研究54:199-230、1995年。
• David Pym とLincoln Wallen。-計算における証明探索${\displaystyle \lambda \Pi }$。G . Huet と G. Plotkin (編)、『Logical Frameworks』、Cambridge University Press、1991 年。
• Didier Galmiche、David Pym。型理論的言語における証明探索：入門。理論計算機科学 232 (2000) 5-53。
• Philippa Gardner.型理論における論理の表現。技術レポート、エディンバラ大学、1992 年。LFCS レポート ECS-LFCS-92-227。
• Gilles Dowek。ラムダπ計算における型付けの決定不可能性。M. Bezem、JF Groote (編)、型付けラムダ計算とその応用。コンピュータサイエンス講義ノート第664巻、139-145、1993年。
• David Pym.一般論理における証明、探索、計算。博士論文、エディンバラ大学、1990 年。
• David Pym. -計算のための統一アルゴリズム。International${\displaystyle \lambda \Pi }$ Journal of Foundations of Computer Science 3(3), 333-378, 1992.

• 特定の論理フレームワークと実装 ( Frank Pfenningが管理するリストですが、1997 年からリンクがほとんど切れています)