証明木作成のための GUI 構築
櫻井加奈子

1(指導教官:浅井健一)

はじめに

3

シーケント計算証明木は論理学、自然言語学の推論だけでなく、プ

本節では、Wadler [2] の定式化を使ったシーケントログラミング言語学の型推論等でも用いられている。

計算を導入する。シーケント計算の推論規則の一部を証明木の記法を示す。

示す。

FormulaA, B ::= X | A ∧ B | A ∨ B | ¬A | A ⊃ B
Antecedent Γ ::= A1 , ..., Am
SuccedentΘ ::= B1 , ..., Bn• 命題 S1 から命題 S2 が推論される時
S1S2Γ⇒ΘΓ ⇒ Θ, A Γ ⇒ Θ, BId∧RA⇒AΓ ⇒ Θ, A ∧ B• 複数の命題 (S1 , S2 , ..., Sn ) から命題 Sn+1 が推論される時
S1 S2 ... Sn
Sn+1Sequent(式)B, Γ ⇒ ΘA, Γ ⇒ Θ∧LA ∧ B, Γ ⇒ Θ A ∧ B, Γ ⇒ Θ• 命題 S が前提なしに成り立つ時 (公理)S4

例えば、シーケント計算で、a∨b∧c ⇒ (a∨b)∧(a∨c)

LablTk
本研究では OCaml のプログラムから Tk [1, 3] へのが正しいことを示す証明木は以下のようになる。

アクセス法を提供する LablTk ライブラリを用いた。

b⇒bc⇒ca⇒ab⇒a∨bc⇒a∨ca⇒aa⇒a∨b b∧c⇒a∨b a⇒a∨c b∧c⇒a∨ca∨b∧c⇒a∨ba∨b∧c⇒a∨ca ∨ b ∧ c ⇒ (a ∨ b) ∧ (a ∨ c)

Tk を利用する利点は、容易に GUI の構築ができるこ

最上段の式が全て成り立っているので、最下段の式OCaml のオブジェクトを用いて実装を行った。クラス階層を以下に示す。と、他言語への移植が比較的容易なこと、OS への依存が低いことが挙げられる。

5が正しいことが証明される。

実装

Tree2

研究背景

Element

手で証明木を描く場合の主な問題点を挙げる。

Organ• 描こうとする証明木がどれだけのスペースを必要とするのかを推論する前に考えなければならない。

Line

Formula

Text

Judge

Horizontal

Ant
Suc

Infer
Id infer• 証明に試行錯誤が必要な時に、何度も描き換えなくてはならない。

Frame

Label
VarAnd
Or
Not
Imply

証明木を作成するための基本的な要素を Element クラスとし、必要最低限の機能を与えた。証明木を構成• 単一化する際に型推論等では証明木の至るところを書き換えなくてはならない。

するための道具として、Organ クラスを作成し、機能別にクラスを作成した。Organ クラスに属する各クラスは次のように証明木を構成する。

証明木を描くことはそれ自体が目的ではなく、証明のためには証明木を簡単に描けること、証明木を描く

Judge : 各段の式を作成する。最下段の式はユーザが入力した論理式をもとに作成されるが、推論規則十分なスペースが確保されていることが必須となってを適用すると上段の式を作成し、Infer クラスを作くる。以上を考慮に入れた上で、本研究では証明木作る。他の推論規則を導入する際には、Judge クラス成のための GUI 構築を行う。今回は、GUI 構築の手の Apply メソッドに加えれば良い。

木の本質にあるものを読み取ることが目的である。そFormula · · · Formula ⇒ Formula · · · Formula
£¢
£
¢
Ant
Suc

法を示すための一例としてシーケント計算の推論規則を用いた。

13

Infer : 3 つのオブジェクト (Judge、Line、Frame)を縦に並べる。上段の Frame では複数の Judge もし
くは Infer を配置することができる。Infer クラスは再帰的な構造をしており、証明木を上に積み上げる。
¤ FrameJudge/Infer · · · Judge/Infer

Judge
Id infer : 公理を適用した Judge に上線を付け、推図 2: 証明木作成画面

論規則をそれ以上適用できなくする。

Judge

6

挙動

推論を行いたい論理式を Antecedent(空でも良い) とSuccedent に入力し (図 1)、Start ボタンを押すと最下段の式が作成される。各機能の中から Apply を選択し、推論規則を適用したい論理式をクリックすると、適用
図 3: 証明木完成画面

可能な論理式に青枠が付く。Go ボタンのクリックにより、上段に規則適用後の論理式が生成される。3 節の ∧L のように、同じ推論規則でも 2 項ある Formula

7の内どちらかを選択しなければならない場合はポップ

まとめ
本稿では証明木作成のための GUI 構築の基礎を述

アップウインドウが表示されるので、選択する (図 2)。

べた。構想としては汎用性のあるものとなっている。

これを繰り返し、証明木を完成させる (図 3)。

簡単な操作で証明木が描けるため、研究目的だけでな各機能を表にまとめる。

ApplyId

公理を適用し、不要な Formula を削除。
可能な限り、全ての式に Id を適用。

Highlight

同期している Formula に青枠表示。

Remove用できると考える。

推論規則を適用。

All IdTex

く、初めて証明木に触れる学生の教育支援としても利

8

今後の課題
Id infer オブジェクトを生成する際に、Judge の Ant

TEX コードを別ファイルに出力。
♣ １節の証明木はこの機能を用いて作成と Suc にある論理式を同じものとして見なしたい (単したものである。

まうと、Remove する際に元に戻すことができなくなっ証明木の一部分を消去。てしまうので、Uniﬁcation のための構造を見直す必要

一化、Uniﬁcation)。しかし、完全に同じものとしてしがある。

図 3 では、Highlight 機能によって同じ意味を持つ

また、より広範な使い方ができるように機能を追加

Formula が青枠で囲まれている。型付き言語においては表現が異なるものであっても同じ意味を持つことがしていくこと、他の推論規則を組み込むために、ユーザがマクロを書けるようにしていくことが今後の課題ある。この機能は今後型付き言語を導入する際、ユーである。

ザが視覚的に捉えやすいように考慮したものである。
しかし、シーケント計算でも論理式がどのように変化参考文献していくのかを見るためには有益であると思われる。

[1] Mark Harrison and Michael McLennan, Eﬀective Tcl/Tk Programming, Massachusetts : Addison Wesley (1998).
[2] Philip Wadler, “Call-by-Value is Dual to Callby-Name”, In ICFP’03, pp. 189–201 (August2003).
[3] http://homepage3.nifty.com/kaku-chan/tcl tk/,Tcl/Tk で Windows プログラミング.

図 1: 初期画面14