OTTER本


  • Global Moderator

    この「天秤のコインのパズル」の例の残念なところは、

    • 最初の例としてotterへの入力コードが分かりやすいとは思えない。読者が初めて出会う例なのだから、できるだけコメントを豊富に、読みやすくしたほうが良いのではないか?→ちゃんと内容の説明は本にありますが。
    • 本の説明(p.2)では、計11枚のコイン(そのうちの1枚が偽)と書いてあるのに、なぜか、レポジトリから入手したprg0-1.inの先頭コメント(前述)では、12枚のコインとなっていること。どちらなのか?→コードを見ると、11枚が正しいことが分かります。

    です。


  • Global Moderator

    OTTERへは、単純には2つのリストを与えるようです。1つは sos (set of support)のリスト、もう一つは usable リストです。さきほどの prg0-1.out でも先頭に出てきています。

    私が理解したところによると、sosには証明(演繹)に対する証拠を入れます。実験科学なら、観察事実に相当するものだと思います。usableには、証明(演繹)に使う規則を入れます。実験科学なら、既存の理論や法則に相当するものだと思います。OTTERは、sosリストから1つ(証拠を)取り出して、そこから、usableのリストの要素(規則)を使って演繹できることを作ります。それ(ら)を、新たな証拠としてsosリストに加えます。これを繰り返していき、リストが空になったり、相互に矛盾する証拠が出てくるような、ある種の最適状態を目指すようです。

    usableにリストアップされる規則は、私には分かりにくい形式で書かれます。例えば、

    -Person(x) | Mortal(x).
    

    です。-記号は否定(NOT)を表します。|記号は、または(OR)を表します。「xは人でない、または、xは死すべき定めである」と書かれています。xが人なら、「xは人でない」は成立しないので、前述の「~または~」が成立するためには、後段が正しい、つまり「xは死すべき定め」ということになります。つまり、「xが人なら、xは死すべき定め」ということを、言っているわけです! これらが同じことを言っているというのが、なかなかピンと来ませんでした。難しいです。

    同じように、

    -Bomb(x) | -Ignited(x) | Explode(x).
    

    これは「xは爆弾でないか、xは着火されていないか、xは爆発する」です。「xが爆弾でかつ着火されておれば、爆発する」ということを、とても奥ゆかしく言っています。

    本によると、このように否定をORでつなげたうち、否定でないものが高々一つ含まれたもの全体を、ホーン節と呼ぶそうです。「ホーンぶし」ではなく、「ホーンせつ(Horn clause)」です。
    https://ja.wikipedia.org/wiki/ホーン節


  • Global Moderator

    ここまで理解しても、最初の「天秤とコインのパズル」の usable リストは難解です。特に最初に長大なホーン説があります。

    -solvable(state(hls(XHLS),hs(XHS),ls(XLS),s(XS),rem(XREM)))
    | -PICK(YHLS)
    | -PICK(YHS)
    | -PICK(YLS)
    | -PICK(YS)
    | -$LE(YHLS,XHLS)
    | -$LE(YHS,XHS)
    | -$LE(YLS,XLS)
    | -$LE(YS,XS)
    | -$GT(YHLS+YHS+YLS+YS,0)
    | -$LE(YHLS+YHS+YLS+YS,6)
    | -PICK(ZHLS)
    | -PICK(ZHS)
    | -PICK(ZLS)
    | -$LE(ZHLS+YHLS,XHLS)
    | -$LE(ZHS+YHS,XHS)
    | -$LE(ZLS+YLS,XLS)
    | -$GE(XREM,0)
    | -$EQ(YHLS+YHS+YLS+YS,ZHLS+ZHS+ZLS)
    | -$LE(ZHLS+ZHS+YHLS+YLS,$DIV(3,XREM-1))
    | -$LE(ZHLS+ZLS+YHLS+YHS,$DIV(3,XREM-1))
    | -$LE($PROD(2,$DIFF(XHLS,(YHLS+ZHLS))+$DIFF(XHS,(YHS+ZHS))+$DIFF(XLS,(YLS+ZLS))),$DIV(3,XREM-1))
    | RECORD(parent(state(hls(XHLS),hs(XHS),ls(XLS),s(XS),rem(XREM))),
    left(state(hls(0),hs(ZHLS+ZHS),ls(YHLS+YLS),s($DIFF(XHLS,(YHLS+ZHLS))+$DIFF(XHS,ZHS)+$DIFF(XLS,YLS)+XS),rem(XREM-1))),
    right(state(hls(0),hs(YHLS+YHS),ls(ZHLS+ZLS),s($DIFF(XHLS,(ZHLS+YHLS))+$DIFF(XHS,YHS)+$DIFF(XLS,ZLS)+XS),rem(XREM-1))),
    balance(state(hls($DIFF(XHLS,(YHLS+ZHLS))),hs($DIFF(XHS,(YHS+ZHS))),ls($DIFF(XLS,(YLS+ZLS))),s(XS+YHLS+ZHLS+YHS+ZHS+YLS+ZLS),rem(XREM-1)))).
    

    https://github.com/RuoAndo/otter-book/blob/master/prg0-1.in より

    まだ、謎です。

    余談ですが、「人工知能」が高度になって、それらに問題を解かせるために使う脳の力が、問題自体を解くのに必要な脳の力を越えるようになったとき、「技術的シンギュラリティ」が来るそうです。詳しくは「シンギュラリティは近い―人類が野生に帰るとき」という本を読んで下さい(ウソ)。


  • Global Moderator

    本を読んでも、何が組み込みのシンボルで、何が変数になるのかもよく分からなかったので、マニュアルをざっと見ました:
    https://www.mcs.anl.gov/research/projects/AR/otter/otter33.pdf

    • $で始まるのは組み込みのシンボルで予約
    • u, v, w, x, y, z で始まる単純項は変数とみなされる。
    • 論理シンボルは、-, |, &, ->, <->, exists, all
    • 大文字小文字の違いはオプションをONにしない限り意味を持たなさそう(明示的には書かれておらず)
    • (組み込みの)コマンド:include(), op(), make_evaluable(), set(), clear(), assign(), list(), formula_list(), weight_list(), lex(), skolem(), lrpo_multiset_status()
    • コメント文は、%で始める。

    まだ分からないことも多いです。


  • Global Moderator

    この本の説明でよくないと思うのは、

    • 説明が安定しない。肝心の場所で説明せず、本のどこにも説明がない事柄があると思えば、複数の場所で繰り返し説明されることもある。3グループに分けて説明を始め、前半2グループについては説明するのに、最後の1グループについて、あたかも忘却したかのように、説明がないこともある。索引はあるが、あまり役に立たない場所を指していることがある。
    • OTTERについて、難しいことを説明せずに省略することがあるが、著者も理解していないような気配がある。省略というのは、全体を理解した人でなければ出来ないはず。

    しかし、自分で調べる手段は残っているので、この本の良さが無くなってしまうわけではないです。


  • Global Moderator

    話変わって、「不思議の国のアリス」の作者、ルイス・キャロルは、数学者であって、この分野(記号論理学)の専門書を書いています:

    "Symbolic Logic, Part I", LEWIS CARROLL, 1897
    https://www.gutenberg.org/files/28696/28696-h/28696-h.htm

    数学パズルの作者でもありました。


  • Global Moderator

    OTTERのソースコードについてくるサンプル(otter-3.3f/examples/auto/salt.in)には、このルイス・キャロルの著作から取られた問題があります。p.192, 問題6「塩とマスタードの問題」です。

    6.
    After the six friends, named in Problem 5, had returned from their tour, three of them, Barry, Cole, and Dix, agreed, with two other friends of theirs, Lang and Mill, that the five should meet, every day, at a certain table d’hôte. Remembering how much amusement they had derived from their code of rules for walking-parties, they devised the following rules to be observed whenever beef appeared on the table:—
    
    (1) If Barry takes salt, then either Cole or Lang takes one only of the two condiments, salt and mustard: if he takes mustard, then either Dix takes neither condiment, or Mill takes both.
    
    (2) If Cole takes salt, then either Barry takes only one condiment, or Mill takes neither: if he takes mustard, then either Dix or Lang takes both.
    
    (3) If Dix takes salt, then either Barry takes neither condiment or Cole take both: if he takes mustard, then either Lang or Mill takes neither.
    
    (4) If Lang takes salt, then Barry or Dix takes only one condiment: if he takes mustard, then either Cole or Mill takes neither.
    
    (5) If Mill takes salt, then either Barry or Lang takes both condiments: if he takes mustard, then either Cole or Dix takes only one.
    
    The Problem is to discover whether these rules are compatible; and, if so, what arrangements are possible.
    
    [N.B. In this Problem, it is assumed that the phrase “if Barry takes salt” allows of two possible cases, viz. (1) “he takes salt only”; (2) “he takes both condiments”. And so with all similar phrases.
    
    It is also assumed that the phrase “either Cole or Lang takes one only of the two condiments” allows three possible cases, viz. (1) “Cole takes one only, Lang takes both or neither”; (2) “Cole takes both or neither, Lang takes one only”; (3) “Cole takes one only, Lang takes one only”. And so with all similar phrases.
    
    It is also assumed that every rule is to be understood as implying the words “and vice versâ.” Thus the first rule would imply the addition “and, if either Cole or Lang takes only one condiment, then Barry takes salt.”]
    

  • Global Moderator

    OTTERのマニュアルには、知っているべき用語として以下が挙げられていました:

    variable, constant, complex term, atom, literal, clause, propositional variable, function symbol, predicate symbol, Skolem constant, Skolem function, formula, conjunctive normal form, resolution, hyperresolution, paramodulation

    このうち、自動証明系に特有らしき用語が特に難しく思いました。resolution, hyper-resolution, paramodulation などです。resolution(導出)は、この世界では特有の意味を持つようです:
    https://ja.wikipedia.org/wiki/導出原理

    論理式が複数あったとき、それらから効率的に充足不能性というものを調べる手法らしいです。やはり基礎がないと追っていくのはたいへんです。



  • @ソム さん
    雑談です。キャロルの論理図と仏教論理学(因明)の論理図と似ていると思ったことがありました。随分昔の事ですし、説明しようにも資料は向こうの書庫にありますので、忘れないための単なる感想です。


  • Global Moderator

    @riffraff さん

    "Symbolic Logic"の扉?にあるこの図ですね。

    以下、https://www.gutenberg.org/files/28696/28696-h/28696-h.htm より拙訳
    図は、under the Project Gutenberg License


    ある三段論法の例

    ===

    君があのウミガメにいちど出会ったという話。あれは、いつも僕にあくびを引き起こす。
    全く興味のないことを聞いている時を除き、僕はあくびをしない。

    ===

    別々の前提。

    0_1538797597462_sorites1.png  0_1538797608509_sorites2.png

    ===

    合わさった前提。

    0_1538797616496_sorites3.png

    ===

    結論。

    0_1538797626754_sorites4.png

    君があのウミガメにいちど出会ったという話には全く興味がない。




  • @ソム さん
    そうです。その図です。図形は違うのですが、コンセプトがディグナーガ以降の因明に似ているなとご紹介の図を初めて見た時に思いました。


  • Global Moderator

    または、

    最初は、|(「または」)ということが、この世界でどういう意味なのか分からず困りました。

    飛行機で「fish or meat?」と聞かれたときには、(たぶんですが)fishまたはmeatのどちらかを選ぶという意味です。このときの「または」、魚肉料理の両方は選べず、選択は排他的です。これを「排他的OR」と呼ぶと思います。深夜食堂でも出てきた、XORです。両方が真のときには、全体は偽となります。

    自動証明、あるいは、記号論理学の世界で、「または」の意味がどうなのか、OTTER本には説明がありませんでした。推測は出来たのですが、モヤモヤします。スマリヤンの「記号論理学」を読むと「論理結合子」として、「論理和、選言、(「または」)」として説明がありました:

    論理和
    命題pおよびqの少なくとも一方(両方でもよい)が真であることを意味する命題を "pVq" と書く。pVqは「pとqのいずれか」、またはより簡潔に「pまたはq」と読む。命題pおよびqの少なくとも一方が真ならば、命題pVqは真となり、pおよびqがともに偽ならば、命題pVqは偽となる。

    こういうことがちゃんと書いてあるのが教科書のよいところだと思います。



パズルハウスへの接続が失われたと思われます。再接続されるまでしばらくお待ちください。