ラーチプルーバー

Larch Prover （略してLP ）は、多重ソートされた一階述語論理のための対話型定理証明システムです。1990年代にMITなどで回路、並行アルゴリズム、ハードウェア、ソフトウェアの設計を推論するために使用されました。 ^[1]

正しく述べられた推測の証明を自動的に見つけようとするほとんどの定理証明器とは異なり、LP は、ユーザーが推測の欠陥を見つけて修正するのを支援することを目的としていました。これは、設計プロセスの初期段階での主な作業です。LP は、大規模な問題に効率的に対応し、多くの重要なユーザーアメニティを備えており、比較的初心者のユーザーでも使用できます。

LPは、MITコンピュータサイエンス研究所のStephen GarlandとJohn Guttagが、DECシステム研究センターのJames HorningとJames Saxeの協力を得て、形式仕様に関するLarchプロジェクトの一環として開発しました。^[2]これは、Pierre Lescanne、^[3] Randy Forgaard ^[4]がDavid DetlefsとKatherine Yelickの協力を得て開発したREVE 2等式項書き換えシステムを拡張したものです。等式項書き換え（結合-可換演算子を持つ項の場合）、ケース、矛盾、帰納、一般化、および特殊化による証明をサポートしています。

LP はCLUプログラミング言語で書かれました。

ソートE、Sを宣言する
変数 e、e1、e2: E、x、y、z: S を宣言します。
演算子を宣言する
  {}: -> S
  {__}: E -> S
  挿入: E, S -> S
  __ \union __: S, S -> S
  __ \in __: E, S -> ブール
  __ \subseteq __: S, S -> ブール
  ..

セット名 setAxioms
アサート
  {} によって生成された S をソートし、挿入します。
  {e} = 挿入(e, {});
  ~(e \in {});
  e \in insert(e1, x) <=> e = e1 \/ e \in x;
  {} \subseteq x;
  挿入(e, x) \subseteq y <=> e \in y /\ x \subseteq y;
  e \in (x \union y) <=> e \in x \/ e \in y
  ..
名前拡張性を設定する
\A e (e \in x <=> e \in y) => x = y であると主張

セット名 setTheorems
e \in {e} を証明する
qed

\E x \A e (e \in x <=> e = e1 \/ e = e2) を証明します。
  x を insert(e2, {e1}) に特化して再開する
qed

% 和集合に関する 3 つの定理 (外延性を用いて証明)

x \union {} = x を証明する
  外延性において y を x \union {} でインスタンス化する
qed

x \union insert(e, y) = insert(e, x \union y) であることを証明します。
  矛盾による履歴書
    集合名補題
    クリティカルペア *外延性を伴うヒプノシス
qed

ac \unionを証明する
    矛盾による履歴書
      集合名補題
      クリティカルペア *外延性を伴うヒプノシス
    矛盾による履歴書
      集合名補題
      クリティカルペア *外延性を伴うヒプノシス
qed

% 部分集合に関する3つの定理

証明方法の設定 =>、正規化

e \in x /\ x \subseteq y => e \in y を x に関する帰納法で証明する
      ケース別に再開 ec = e1c
        集合名補題
        完了
qed

x \subseteq y /\ y \subseteq x => x = y を証明する
    集合名補題
    e \in xc <=> e \in yc を <=> で証明する
        完了
        完了
    外延性において x を xc で、y を yc でインスタンス化する
qed

(x \union y) \subseteq z <=> x \subseteq z /\ y \subseteq z を x 上の帰納法により証明する
qed

% 代替帰納法の規則

{}、{__}、\unionによって生成されたソートSを証明する
    集合名補題
    誘導による履歴書
      クリティカルペア *GenHyp と *GenHyp
      critical-pairs *InductHyp と補題
qed

Pascal André、Annya Romanczuk、Jean-Claude Royer、および Aline Vasconcelos、「Larch Prover を使用した UML クラス図の一貫性のチェック」、2000 International Conference on Rigorous Object-Oriented Methods の議事録、1 ページ、ヨーク、英国、BCS Learning & Development Ltd.、スウィンドン、GBR、2000 年 1 月。

Boutheina Chetali、「Larch Prover を使用した並行プログラムの形式検証」、 IEEE Transactions on Software Engineering 24:1、46 ～ 62 ページ、1998 年 1 月。doi: 10.1109/32.663997。

Manfred Broy、「LP (Larch 証明アシスタント) を使用したソフトウェア仕様と検証の経験」、 Formal Methods in System Design 8:3、221 ～ 272 ページ、1996 年。

Urban Engberg、Peter Grønning、および Leslie Lamport、「TLA による並行システムの機械的検証」、 Computer-Aided Verification、G. v. Bochmann および DK Probst 編集者、Proceedings of the Fourth International Conference CAV'92)、 Lecture Notes in Computer Science 663、Springer-Verlag、1992 年 6 月、44 ～ 55 ページ。

Urban Engberg、「行動の時間的論理における推論」、BRICS 博士論文シリーズ DS 96–1、コンピュータサイエンス学部、オーフス大学、デンマーク、1996 年 8 月。ISSN 1396-7002。

Stephen J. Garland および John V. Guttag、「抽象データ型についての推論のための帰納的方法」、 プログラミング言語の原理に関する第 15 回 ACM シンポジウム、219 ～ 228 ページ、カリフォルニア州サンディエゴ、1988 年 1 月。

Stephen J. Garland および John V. Guttag、「LP: The Larch Prover」、第 9 回国際自動演繹会議、 コンピュータ サイエンスにおける講義ノート310、748 ～ 749 ページ、イリノイ州アルゴンヌ、1988 年 5 月。Springer-Verlag。

Stephen J. Garland、John V. Guttag、Jørgen Staunstrup、「LP を使用した VLSI 回路の検証」 、 The Fusion of Hardware Design and Verification、329 ～ 345 ページ、スコットランド、グラスゴー、1988 年 7 月 4 ～ 6 日。IFIP WG 10.2、北ホラント。

Stephen J. Garland および John V. Guttag、「LP (Larch Prover) の概要」、 Third International Conference on Rewriting Techniques and Applications Lecture Notes in Computer Science 355、137 ～ 151 ページ、ノースカロライナ州チャペルヒル、1989 年 4 月。Springer-Verlag。

Stephen J. Garland および John V. Guttag、「LP を使用した仕様のデバッグ」、 プログラミングの概念と方法、ガリラヤ湖、イスラエル、1990 年 4 月 2 ～ 5 日。IFIP WG 2.2/2.3、北ホラント。

Stephen J. Garland および John V. Guttag、「A Guide to LP: the Larch Prover」、MIT Laboratory for Computer Science、1991 年 12 月。Digital Equipment Corporation Systems Research Center Report 82 (1991) としても出版されています。

Victor Luchangco、Ekrem Söylemez、Stephen Garland、および Nancy Lynch、「並行アルゴリズムのタイミング特性の検証」、 FORTE '94: Seventh International Conference on Formal Description Techniques、259 ～ 273 ページ、ベルン、スイス、1994 年 10 月 4 ～ 7 日。Chapman & Hall。

Ursula Martin と Michael Lai、「完了定理証明器を使用したいくつかの実験」、 Journal of Symbolic Computation 13:1、1992 年、81 ～ 100 ページ、ISSN 0747-7171。

Ursula Martin および Jeannette M. Wing 編、 『First International Workshop on Larch』、『Proceedings of the First International Workshop non Larch』、マサチューセッツ州デダム、1992 年 7 月 13 ～ 15 日、Workshops in Computing、Springer-Verlag、1992 年。

• ミシェル・ビドワとロルフ・ヘニッカー、「LP による観測定理の証明方法」、18～35 ページ
• Boutheina Chetali と Pierre Lescanne、「LP の演習: 非復元除算回路の証明」、55 ～ 68 ページ
• Christine Choppy と Michel Bidoit、「ASSPEGIQUE と LP の統合」、69 ～ 85 ページ
• Niels Mellergaard および Jørgen Staunstrup、「回路に対する証明義務の生成」、185 ～ 200 ページ
• EA スコットと KJ ノリー、「LP を使用した言語 PL ₀ ⁺の学習」、227 ～ 245 ページ
• フレデリック・ヴォワザン、「Larch Prover の新しいフロントエンド」、282 ～ 296 ページ
• JM Wing、E. Rollins、A. Moorman Zaremski、「Larch/ML に関する考察と LP の新しい用途」、297 ～ 312 ページ

Toh Ne Win、Michael D. Ernst、Stephen J. Garland、Dilsun Kirli、および Nancy Lynch、「分散アルゴリズムの検証におけるシミュレートされた実行の使用」、 Software Tools for Technology Transfer 6:1、Lenore D. Zuck、Paul C. Attie、Agostino Cortesi、および Supratik Mukhopadhyay (編集者)、67 ～ 76 ページ。Springer-Verlag、2004 年 7 月。

Tsvetomir P. Petrov、Anya Pogosyants、Stephen J. Garland、Victor Luchangco、および Nancy A. Lynch、「同時タイムスタンプのアルゴリズムのコンピュータ支援検証」、 Formal Description Techniques IX: 理論、アプリケーション、およびツール (FORTE/PSTV)、Reinhard Gotzhein および Jan Bredereke (編集者)、29 ～ 44 ページ、Kaiserslautern、ドイツ、1996 年 10 月 8 ～ 11 日。Chapman & Hall。

James B. Saxe、Stephen J. Garland、John V. Guttag、James J. Horning、「回路設計における変換と検証の使用」、 『システム設計における形式手法』 3:3 (1993 年 12 月)、181 ～ 209 ページ。

Jørgen F. Søgaard-Anderson、Stephen J. Garland、John V. Guttag、Nancy A. Lynch、および Anya Pogosyants、「コンピュータ支援シミュレーション証明」、Fifth Conference on Computer-Aided Verification (CAV '03)、Costas Courcoubetis (編集者)、Lecture Notes in Computer Science 697、305 ～ 319 ページ、ギリシャ、エロウンダ、1993 年 6 月。Springer-Verlag。

Jørgen Staunstrup、Stephen J. Garland、および John V. Guttag、「回路記述の局所的検証」、 Automatic Verification Methods for Finite State Systems、Lecture Notes in Computer Science 407、349 ～ 364 ページ、フランス、グルノーブル、1989 年 6 月。Springer-Verlag。

Jørgen Staunstrup、Stephen J. Garland、および John V. Guttag、「Larch Prover を使用した回路記述の機械化された検証」、 Theorem Provers in Circuit Design、Victoria Stavridou、Thomas F. Melham、および Raymond T. Boute (編集者)、 IFIP Transactions A- 10、277 ～ 299 ページ、オランダ、ナイメーヘン、1992 年 6 月 22 ～ 24 日、北ホラント。

Mark T. Vandevoorde および Deepak Kapur、「Distributed Larch Prover (DLP): 書き換えルール ベースの証明器の並列化の実験」、 International Conference on Rewriting Techniques and Applications RTA 1996、 Lecture Notes in Computer Science 1103、420 ​​～ 423 ページ。Springer-Verlag。

Frédéric Voisin、「Larch 証明器用の新しい証明マネージャとグラフィック インターフェイス」、 International Conference on Rewriting Techniques and Applications RTA 1996、 Lecture Notes in Computer Science 1103、408 ～ 411 ページ。Springer-Verlag。

Jeannette M. Wing および Chun Gong、「Larch Prover の使用経験」、 ACM SIGSOFT ソフトウェア エンジニアリング ノート15:44、1990 年 9 月、140 ～ 143 ページ https://doi.org/10.1145/99571.99835

• ラーチのウェブサイト
• LP のオンライン ドキュメント