リリカル☆Lisp開発日記 » Blog Archive » 機械もすなる論理学を機械にやらせてみた

TL;DR: Prologの双方向代入最高！ はじめに 8年ほど前に『論理学を作る』という本を読みまして、そこにタブローの方法と呼ばれる論理式の集合が充足可能か調べるアルゴリズムが載っていました。「暇があったらいつか実装してみるか」と思っていたら8年も経ってしまいましたが、暇があったので実装してみました。Prologで。 タブロー（tableau）とは要は木で、木を書くと論理式の集合が充足可能かどうか分かるというものです。こういう時にはWikipediaさんに説明を任せたいのですが、日本語版にはまるで情報がありません。英語版はきちんと書いてあるっぽいので気になる方はそちらを参照してください。 少しだけ説明をすると、与えられた論理式の集合をルートとして、その中の複合式を充足させるのに必要な（より小さな）式を子として木を作っていき、ルートからリーフに至る経路にAと¬A (Aはリテラル) の両方

[theatrical]

「論理学を作る」は、欲しいなって思ってたなぁ。買おうかな