sazare
commented
4 years ago Computational LogicやResolutionの教科書にUnificationについて書かれた章はあるが、あまりちゃんと読んでいない。 このpdfがなかなかページ数も多く、総括的だったので読み始めたら面白かった。 半分以上が等号を含むunificationの話なので、ちょっと期待とはずれているかもしれない。 とはいえunificationとは等しくするものなので、等号とは切ってもきれないものではある。
unification のいろいろな実装の差について知りたいのだけれど、なかなかそういう論文はない。 githubで実装をさがせということなのだが、なかなか手が伸びていない。 まずは代入の表現や代入操作の定義の違いを知りたいということもあって、調べている。
by Franz Baader, Wayne Snyder http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf HANDBOOK OF AUTOMATED REASONING 2001 の8章で、pdfとして公開されていた。最終稿かどうかは不明。