定理証明手習い (2) J-Bobを動かす

「自分で動かしながら楽しみたい」という読者のために、J-Bobという簡素な定理証明支援系を用意してあります。

必須じゃないという書き方ですね
でもせっかくですから動かしてみたい

まずはThe Little Proverのページにアクセスしてみます
J-BobはGitHubからダウンロードできます
SchemeやRacketでも動くって書いてありますね
よかったよかった
Racketで動かすにはDracuraっていうパッケージがいるようです
でもSchemeで動くならそれでよさそうな気もするけど
どっちでやってみるかな

まずはDracuraから見てみよう
DracuraはACL2のためのプログラミング環境です、か
なるほど
DrRacketとACLをくっつけてぐちゃっとするとDraculaになりそうだな
uが足りないか
DrRacketは入ってるから、まずACL2を動かさないと
なかなか大変だな

ACL2からたどっていくとMac OS Xにはpre-built binary distributionがあるらしい
さらにACL2 SedanっていうバイナリやドキュメントやEclipseベースの開発環境が
全部入りのがあるって書いてあるな
別にRacketにこだわらなきゃこれ入れとけば済むのかな
でも今ネット環境がなくてiPhoneのテザリングでJDKとEclipse落とすのはちょっとつらい

・・・
考えるのに疲れてScheme版の方を試すことに
RacketでScheme版を動かす手順も書いてあります

以下、LittleProverフォルダを使うことにします

GitHubからj-bobをダウンロード
schemeフォルダをj-bobという名前でLittleProverフォルダに保存
DrRacketのLanguageメニューからChoose Languageを選択
Other Languages、R5RSを選択
Show Detailsを選択してDisallow redefinition of initial bindingsのチェックを外す
FileメニューのNewで新規ファイルを作成し、test.scmという名前でLittleProverフォルダに保存

で以下のコードを入力してやればいけそう

(load "j-bob/j-bob-lang.scm")
(load "j-bob/j-bob.scm")

意味はわかりませんがちょっと先回りしてテスト

> (defun chapter1.example1 ()
  (J-Bob/step (prelude)
    '(car (cons 'ham '(eggs)))
    '(((1) (cons 'ham '(eggs)))
      (() (car '(ham eggs))))))
> (chapter1.example1)
'ham

どうやら使えるようになったみたいです
今はACL2を使いたいってわけではないのでこれでいいかな

kb84tkhrのブログ

何を書こうか考え中ですあ、あと組織とは関係ないってやつです個人的なやつ

定理証明手習い (2) J-Bobを動かす