モナ★MONAのこと
★モナMONAのこと
MONA （http://www.brics.dk/mona/） は式を有限オートマトンに変換するツール。
検索パターンや時相論理の属性値を持つようなリアクティブシステム（こっちからなんかすると反応が返ってくるようなシステムのこと）やパーズ木（ 解析木-構文分析の結果を図示したもの）の制約を表すようなものを対象としている。
MONAは変換したオートマトンを分析してそれが妥当であるとか、あるいは反例（仮説に反対の論拠として用いられる反事実, 反証のこと）を出力してくれるありがたいツールだ。
MONAには１つあるいは２つのsuccessor関数の弱二次理論（Weak Second-order Theory）を決定手続きを取得する機能を持っている。
１つのsuccessor理論は一般的にはWS1Sと略されているもので、自然数の有限集合を二階量化子で拡張。successor関数と呼ばれる単項演算+1を持つもの。
WS2Sは木構造を一般化したもの。
MONAの呼び名はこの理論がmonadic（単一の論拠を持つ）単項二階論理であることに由来する。
（原文）
MONA is a tool that translates formulas to finite-state automata. The formulas may express search patterns, temporal properties of reactive systems, parse tree constraints, etc. MONA analyses the automaton resulting from the compilation and prints out "valid" or a counter-example.
MONA implements decision procedures for the Weak Second-order Theory of One or Two successors (WS1S/WS2S).
The theory of one successor, known as WS1S, is a fragment of arithmetic augmented with second-order quantification over finite sets of natural numbers. Its first-order terms denote just natural numbers.
The theory has no addition, since that would make it undecidable, but it has a unary operation +1, known as the successor function.
WS2S is a generalization to tree structures. Since the theories are monadic一価の second-order logics, we call our tool MONA.
◇ためになったサイト◇
・MONAで正規表現にマッチする例を生成するCommentsAdd Star
http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20080727
・細谷研究室 演習３課題 「MONAを使おう」
http://arbre.is.s.u-tokyo.ac.jp/enshu3/mona/index.html
■MONAのインストール■
http://www.brics.dk/mona/download.html
からexeとcygwin.dllをダウンロードして一つのフォルダに入れる。
テキストファイルに例えばtest.monaとして下記を保存。
ws2s;
guide d0->(a,b), a->(a,a), b->(b,b);
universe ua:0, ub:1;
var2 [ua] A;
var2 [ub] B;
ex1 [ua] p1,p2,p3,p4,p5:
A = {p1,p2,p3,p4,p5} &
p1
実行結果
C:\ProgramFiles2\MONA>mona test.mona.txt
MONA v1.4-13 for WS1S/WS2S
Copyright (C) 1997-2008 BRICS
PARSING
Time: 00:00:00.00
CODE GENERATION
DAG hits: 137, nodes: 91
Time: 00:00:00.00
REDUCTION
Projections removed: 2 (of 34)
Products removed: 3 (of 42)
Other nodes removed: 2 (of 16)
DAG nodes after reduction: 85
Time: 00:00:00.01
AUTOMATON CONSTRUCTION
100% completed
Time: 00:00:00.42
Automaton has 18 states and 32 BDD nodes
ANALYSIS
Free variables are: A, B
A counter-example is:
Booleans:
XX
Universe ua:
()
Universe ub:
()
A satisfying example is:
Booleans:
XX
Universe ua:
(1X,(1X,(),(1X,(),(1X,(),(1X,(),())))),())
Universe ub:
(X1,(X1,(X1,(X1,(),(X1,(),(X1,(),(X1,(),())))),()),()),())
Total time: 00:00:00.43
★RacerProのこと
http://www.racer-systems.com/products/racerpro/index.phtml
の解説より。。。
RacerProは大変効率の良いタブロー計算機能を持つ知識表現システムである。
DL（Description Logic記述論理）分野から生み出されたソフト。DLはセマンティックウェブ（自然言語だけではなくマシンのようなエージェントも扱えるような形式のWEBコンテンツを考えた世界というかそういうWEB環境を目指すプロジェクト）においてオントロジー言語を標準化するものである。RacedrProはOWL（オントロジーを用いてデータ交換を行うためのマークアップ言語）を基礎とするセマンティックウェブオントロジーのためのシステムとしても用いることが出来る。
一方ではその大量にデータ記述の集合を扱えるという特徴ゆえにセマンティックウェブ情報のリポジトリとしても有用。
また忘れてはならないのは、Kmのような様相論理学（□とか◇を使うやつ）の記述にも使えるということだ。
概念記述であるTboxes（スキーマやクラスに近いもの）と個体記述をAbox（インスタンスに近いもの）のための推論する機能もある。
記述論理DLについては ALCQHIR+別名SHIQを実装。
■RacerProのインストール■
ダウンロードは
http://www.racer-systems.com/
から。1ヶ月お試し出来る。
セットアップするとPC内で下記ポートを使ってサーバとして動くリクエスト待ちになる。
HTTP service enabled for: http://localhost:8080/
TCP service enabled for: http//localhost:8088/
★（ときどきふざけた）用語メモ
■木オートマトン 文字列の代わりに木を入力するオートマトン
なおXMLは木のサイズ（枝の数）が決まっていない木だが、これを2分木オートマトンとみなして簡易な型のモデルを作ることが出来る。
■背理法 とは
indirect あるいは a reduction to absurdity あるいは Reductio ad absurdum ともいう。
後期ラテン語（3-6世紀に学者たちが使ったラテン語のことである）でreduction to the absurd 「ばかげたこと、不条理なことを導く」の意。アーレフの上祐史浩がTVで「こんなばかげたことがあるか」とプラカードを叩いて捨てたパフォーマンスは背理法をビジュアル化したものである。
「もし彼女が北島マヤならば横浜中華街にあるラーメン屋の住み込み店員である母のもとで貧しい幼年期を過ごしていたはずだ」を背理法で証明する場合、
彼女が北島マヤであり、しかも「横浜中華街にあるラーメン屋の住み込み店員である母のもとで貧しい幼年期を過ごして」いなかったとした場合に、矛盾が生じることを証明すればよい。
■演繹的証明 Deduction proof とは
文の列であって、ある出発点となる「前提」あるいは「所与の（すでにはっきりしている）文」（複数個でもよい）から正しい「結論」を導くもの。すでにはっきりしている事実から正しい推論の法則にしたがって導かれなければならない。帰納的証明はInductive proof
■定理 theorem とは
仮定Hから結論Cが証明されたときの、文「もしHならばC」（例 もしa=1ならばa+a=2）を定理と呼ぶ。
■有限である finite とは
集合Sはある整数nについて「Sはちょうどn個の要素を持っている」と言えるときSは有限であるという。
| S | =nと書く。 | S | はSの要素の個数という意味。 |
■必要条件 necessary condition
P ならば Q である が真のときのQをPが成り立つための必要条件という
1 : a state of affairs that must prevail if another is to occur : PREREQUISITE
例「息を吸うことは人が生きてゆくために必要だ」の場合だと「人が生きてゆく」が必要条件となる。直感での理解と違ってくるのでこんがらがりそうな所。
■十分条件 sufficient condition
P ならば Q である が真のときのPをQ が成り立つための十分条件という 「あなたがもし人間ならば哺乳類である」という文がある場合、哺乳類であることは人間であることの必要条件であるが、十分条件ではない。
