著者

近藤 久 栗原 正仁 大内 東

雑誌

全国大会講演論文集

巻号頁・発行日

vol.第40回, no.データ処理, pp.974-975, 1990-03-14

---

一般に項書き換えシステムの停止性を検証することは決定不能な問題であることが知られているが、Dershowitzによって提案された単純化順序を用いることによって、特定のクラスの項書き換えシステムの停止性を検証することが可能である。本稿では単純化順序として辞書式経路順序を仮定するが、本稿の考え方は他の順序を仮定しても成り立つ。辞書式経路順序を用いるためには、項を構成している演算子の集合上の半順路を決定しなければならない。この半順路を決定する問題は、多くの不必要な探索、矛盾の再発見、不必要な推論を行う。これらの問題点を避けて効率よい問題解決を実現するためのアーキテクチャとしてATMSが提案されている。本稿では、ATMSを用いた停止性検証システムの開発について述べる。