トップ «前の日記(2007-11-22) 最新次の日記(2007-11-24)» 月表示編集

日々の流転

2007-11-23 [長年日記]

λ. Molle (MOdal Logic Loony Evaluator)

最近様相論理の定理証明器を少し探していて見つけた、タブローによる証明器。 Javaで書かれていて簡単に試せる。ただ、複数の様相を扱えず、またKでの証明しか扱えないっぽい。

スクリーンショット

□(A→B)→□A→□B を証明させた場合
□(A∨B)→□A∨□B を証明させた場合
□(A∨B)→□A∨□B の反例のクリプキ構造

Tags: modal-logic

[ツッコミを入れる]