人間は、新しい事実を知ることにより、以前の結論を翻す非単調推論を行う ことがある。そのような推論の形式化にReiter(1980)によって提唱された デフォルト論理がある。デフォルト論理では、デフォルトという推論規則に よって非単調性を表現する。また、前提知識とデフォルトを用いて推論される 知識の集合を拡張という。デフォルト論理を用いた推論、すなわち デフォルト論理における定理証明は、与えられた論理式が属する拡張を 計算することである。それに対して、タブロー法に基づいたアルゴリズムが Amatiら(1996)によって提案された。
本論文では、Amatiらのアルゴリズムをもとに、タブロー法に基づく デフォルト論理の拡張計算システムを実現した。また、このシステムを用いて、 デフォルト論理を用いた種々の知識表現に対して推論が実現されていることを 確認した。