The ProofDisplay is a rich graphical interface used to to interact with AProS. In the ProofDisplay one can view both the resulting proof and each step in the search in a number of formats.

ProofDisplay は Carnegie Mellon 大学の Automated Proof Search プロジェクトの証明検索エンジン AProS の GUI です.


  • Demo 版ですが,最小,直観主義,古典論理の各範囲から命題,一階述語論理の定理式のサンプルが選べます.


  • Webstart 用ですので,実行には Java 環境とネットワーク環境が必要です.
  • 次をクリックし,(Firefoxの場合)「プログラムで開く」を選択,OKを押してください(初回のみ確認のメッセージなどが出ます).
  • 起動したらメニューの「Tools」→「Choose Assertion Category」→「Standard Problem Files」から適当な定理式を選び,C-p(コントロールキーを押しながら,pを押す) で自然演繹による証明が検索,表示されます.


添付ファイル: file20130929-pd.png 1768件 [詳細]

トップ   編集 凍結 差分 バックアップ 添付 複製 名前変更 リロード   新規 一覧 単語検索 最終更新   ヘルプ   最終更新のRSS
Last-modified: 2015-01-09 (金) 18:44:24 (2518d)