一階論理タブローによるモデル生成の再帰性検出とモデル表現の一般化

摘要

新しいモデル生成手続きMEタブローについて提案し概観した。本手法により，従来のモデル生成手法では，停止しないような節集合に対して，モデルの有限記述を導入することにより停止することを例によって示した。今後の課題は，MEタブロー上での極小モデルの生成[5]および，応用分野への適用である。