スポンサーサイト

上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

トートロジーを判定するプログラム

開発中のプログラムに必要だったので、最近は構文解析についてちょっと調べていました。
ちょうど、夏休みに論理学に触れたということもあったので、それに関連して、
(命題論理の)論理式がトートロジーかどうかを判定するプログラム
を組んでみました。

Tags : 数学 論理学 プログラミング

ソースコードはこちらから。
見るときはタブ幅 4 を推奨。
FC2ブログの仕様で拡張子が .txt になってますが、C++のコードです。

[ 仕様 ]
  • 入力
    命題論理の論理式 (詳細は↓)
    • 原子式 は(T,t,F,f,V,v以外の)アルファベット1文字で表す

    • は T または t で表す

    • は F または f で表す

    • 否定 ¬は ~ で表す

    • 連言 ∧は ^ で表す

    • 選言 ∨は V または v で表す

    • 含意 →は > で表す

    • 同値 ⇔は = で表す

    • 論理式は以上の記号と括弧 ( , ) を正しい順序で組み合わせたものに限る。(空白を含んではいけない)

  • 出力
    入力された論理式がトートロジー(恒真式)か矛盾式(恒偽式)かどちらでもないかを示す1行

  • 実行時の引数はなし

  • 演算子の優先順位
    ¬ > ∧ > ∨ > → > ⇔
    括弧をつけなければ、この順序で括弧がついているものとみなされる。

  • 結合法則
    2項間演算子 op について、「A op B op C」は「(A op B) op C」の意味とする。

  • 想定されていない(正しい論理式以外)の文字列を入力した場合の動作は未定義。


[ 中身 ]
概略だけ。

  1. 論理式中の原子式をすべて見つける (findVars関数)

  2. 各原子式に真/偽のいずれかを代入する (subst関数)

  3. 論理式全体の真理値を調べる (parse関数)

  4. トートロジー/矛盾式/どちらでもない が判断できるまで 2. に戻る
    結果的に、どちらでもない 以外なら、2(原子式の種類)回のループになる


  5. ※ 枝刈りも何もせずに全探査してるので、原子式の種類が増えると処理が終わらなくなります。

    構文解析パート

    ・ 論理式のBNF
    <expr> ::= <expr2>|<expr>⇔<expr2>
    <expr2> ::= <expr3>|<expr2>→<expr3>
    <expr3> ::= <term>|<expr3>∨<term>
    <term> ::= <factor>|<term>∧<factor>
    <factor> ::= <primary>|¬<primary>
    <primary> ::= <atomic>|<const>|(<expr>)
    <atomic> ::= A|B|...|E|G|...|S|U|...|Y|Z|a|b|...|e|g|...|r|s|...|y|z
    <const> ::= T|F|t|f


    ※ <expr>が正しい論理式
    ※ プログラム中では原子式にT/Fを代入してから解析しているので、実際は
      <primary> ::= <const>|(<expr>)
      となっている。

    このBNFは、1トークン先読みするだけでどの構文にマッチするかが判断できるので、LL(1)で解析できる。
    なお、今回のプログラムの場合は常に 1トークン=1文字 になる。(簡単のためにそうした。→ を > とするとか。)
    あとは、BNFの通りに書くだけ。

    [ 実行例 ]
    いくつかの有名な定理で検証してみた結果。赤字は入力した文字列、青字は出力された文字列。
    A>A (同一律)
    tautology
    Av~A (排中律)
    tautology
    ~(A^~A) (矛盾律)
    tautology
    ((A>B)^A)>B (Modus ponens)
    tautology
    (A>B)>(~B>~A) (対偶律)
    tautology
    ~(AvB)=~A^~B (De Morganの法則1)
    tautology
    ~(A^B)=~Av~B (De Morganの法則2)
    tautology
    ~AvB=A>B (→の定義)
    tautology
    ((A>B)^(B>C))>(A>C) (推移律)
    tautology
    A^(BvC)=(A^B)v(A^C) (分配律1)
    tautology
    Av(B^C)=(AvB)^(AvC) (分配律2)
    tautology
    A (1つの原子式)
    undetermined
    A^~A (矛盾)
    contradiction


    参考にした書籍・サイト
    中西正和 『記号処理』
    Spaghetti Source
    めも日記 2004/09/01の記事
    d.y.d. 2008/03/05の記事
    スポンサーサイト

コメントの投稿

非公開コメント

プロフィール

fura2

Author : fura2
数学・コンピュータを中心に、考えたこと・やったことを書いていきます。

誤植等を含め、間違いはご指摘いただければ幸いです。

FC2カウンター
検索フォーム
最新記事
最新コメント
最新トラックバック
月別アーカイブ
リンク
RSSリンクの表示
上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。