この論文は、Hornプログラムの論理的性質の証明について、その理論的基礎、自動証明システム、実際的応用に取り組んだ結果を報告する。

　理論的基礎については、まず、Hornプログラムの論理的性質の証明を、与えられたHornプログラムPの最小Herbrandモデルにおいて与えられた拡張確定節Fが成り立つことを示すことと定式化した。これは、Hornプログラミングが成功したのは、計算を記述するための一階述語論理式のクラスを、一般の一階述語論理式のクラスではなく、それにふさわしいHorn節という最小のクラスに限定したからであると考え、Hornプログラムの論理的性質の証明においても、論理的性質を記述するための一階述語論理式のクラスは、一般の一階述語論理式のクラスではなく、それにふさわしい最小のクラスに限定した方がよいと考えたからである。

　理論的基礎については、次に、基本的な証明手続きを提案した。基本的な証明手続きは、与えられた拡張確定節を初期ゴール(根ノード)とし、本体展開、本体たたみ込み、頭部展開、頭部たたみ込み、相殺の五つの推論規則を用いて、各ゴールから新たなサブゴール(子ノード)を生成することを繰り返す。生成された証明木の葉ノードのサブゴールが全てtrueになると、最初に与えられた拡張確定節FがプログラムPの最小Herbrandモデルにおいて成り立つことが証明されたことになる。証明する論理式のクラスを拡張確定節に限定したことにより、五つの推論規則は、Prologにおける普通のゴールや否定ゴールの実行を拡張した形、あるいは、プログラム変換規則に似た形の簡単なものになった。また、推論規則の適用順序・組み合わせに緩い制限を設けたことにより、五つの推論規則は、適用条件が比較的容易にチェックできて自動化に向いたものになった。

　理論的基礎については、さらに、この基本的な証明手続きが論理的に健全であることを証明した。ここでも、証明する論理式のクラスを拡張確定節に限定したことと、推論規則の適用順序・組み合わせに緩い制限を設けたことにより、健全性の証明における議論が比較的簡単なものになった。

　理論的基礎については、最後に、以前に証明された拡張確定節を補題として利用する推論規則を補足した。これらの推論規則を用いると、現在のゴールを補題に帰着したり、補題を用いて現在のゴールを変形することができる。ここでも、補題が拡張確定節という特定のクラスの論理式であるために、これらの推論規則も比較的簡単なものになった。

　証明システムについては、可能な限り証明を自動的に行なうために、この基本的な証明手続きを、まず、帰納的証明プランを用いる証明手続きに発展させた。基本的な証明手続きは、非決定的に推論規則を適用する形をしているので、そのまま素朴に用いると、非常に多くの証明木を探索しなければならず、自動的に証明木を生成することは難しい。新しく発展させた証明手続きでは、証明木の幹の部分に現れる推論規則・適用対象列のパターンを限定し、この特定のパターンに合致する列だけを探索する。この探索の際、述語の引数に現れる項の深さが、その述語を定義するプログラムの再帰によってどのように変化するかのパターンに注目し、与えられた拡張確定節の中に現れる述語の再帰パターンの整合性を解析し、五つの推論規則をどの順にどの部分に適用できる可能性があるかを示す帰納的証明プランを作る。’初等的’と呼ばれるクラスのプログラムの論理的性質の証明にこの証明手続きを用いると、証明木の主要な部分はこの帰納的証明プランに従って作られるため、探索しなければならない証明木が非常に少なくなる。

　証明システムについては、さらに、補題を利用する推論規則を、この帰納的証明プランを用いる証明手続きに、それにふさわしい形で組み込んだ。特に、補題を用いて現在のゴールを変形する推論規則は、帰納的証明プランを作成する前に補題を用いてより簡単な形に書き換えるものと、帰納的証明プランを作成できなかったときに補題を用いて述語の再帰パターンが整合するように変形するものとに区別して組み込んだ。

　証明システムについては、この帰納的証明プランを用い補題を利用する証明手続きを、実際に並列論理型言語KL1を用いてマルチPSI上に実装した。この実験的な証明システムを用いて、幾つかの中程度のサイズの例についてHornプログラムの論理的性質を自動的に証明することに成功し、帰納的証明プランを用いることによって、かなり複雑な証明木でも自動的に生成することができるようになること、補題を利用することによって、証明木を小さくすることができるようになることを確認した。

　実際的応用については、この証明システムをNビット加算器やNビット並列乗算器などの算術演算組み合わせ回路の検証に適用した。算術演算組み合わせ回路では、ビット列によって自然数が表現され、その機能的な正しさは、ビット列レベルの演算の出力ビット列が表現する自然数が、入力ビット列が表現する自然数に対する自然数レベルの演算(例えば、足し算や掛け算)の結果に一致することと考えられる。

　実際的応用については、まず、Nビット加算器について、適当な補題を用意しておけば、サイズ(ビット長)についての帰納法を用いることによって、その仕様の検証を行なえることを実験的に確認した。また、この証明の過程を検討した結果、入力ビット列、あるいは、出力ビット列が表現する自然数の線形結合を表す述語を新たに導入し、これを用いて仕様を表現し直すことによって、より系統的な検証を行なうことができること、また、補題がなぜ必要であったかも明らかになることを見い出した。

　実際的応用については、次に、二次元のより複雑な構造を持つNビット並列乗算器について、やはり、サイズ(ビット長)についての帰納法を用いることによって、その仕様の検証を行なった。並列乗算器の検証は、順序二分決定グラフを用いた処理では、どのように入力変数の順序を選んでも、順序二分決定グラフのサイズが入力変数の数の指数オーダーで増大し、16ビット程度の並列乗算器でも困難であることがよく知られた問題である。しかし、加算器の検証で見い出したより系統的な検証方法を用いたところ、検証全体は自動的ではないが、ほぼ機械的な手順で検証を行なえることを実験的に確認することができた。

　実際的応用については、さらに、これらの検証の証明時間を測定し、証明木を点検した結果、ビットが0か1かによる場合分けのために証明木が大きくなっていること、しかし、このような場合分けを順序二分決定グラフを用いた処理で簡単に置き換えることはできないことも判明した。

　Hornプログラムについての帰納的証明を行なう他の証明システムのアプローチや、Lispプログラムについて帰納的証明を行なうBoyer-Moore定理証明システムなどのアプローチとの比較も行なった。

　本論文は、「Hornプログラムの論理的性質の証明手続きについて」と題し、9章から成る。一般にHornプログラムを用いた情報処理システムの記述は、基礎となる論理的意味が明晰で、論理的に処理しやすいとされてきたが、このような記述からシステムの論理的性質を厳密に証明する手続きは十分に研究されておらず、複雑で間違った記述をしやすい微妙な問題を扱う上でのネックになっていた。本論文は、Hornプログラムの論理的性質の証明手続きについて検討し、この記述方法の適用範囲の拡大を試みたものである。

　第1章「はじめに」は、本研究の背景と目的について考察し、本研究の意義をまとめるとともに、本論文の構成を述べたものである。

　第2章「準備」は、Hornプログラムを用いた情報処理システムの記述の論理的基礎を概観し、特に、このような記述からシステムの論理的性質を表現する論理式を証明することを厳密に定式化し、本研究の議論に必要な枠組を設定している。

　第3章「基本的な証明手続き」は、Hornプログラムの論理的性質の基本的な証明手続きを提案したものである。すなわち、一階推論のための「本体展開」、「頭部展開」、「相殺」と呼ばれる推論規則、帰納法のための「本体たたみ込み」、「頭部たたみ込み」と呼ばれる推論規則を導入して、通常のHornプログラムのゴールの実行機構やプログラム変換の変換規則の統合を図っている。その結果、幾つかの証明例題について、この基本的な証明手続きを用いて適当な順序で推論規則を適用すると、証明木を作ることができることを明らかにしている。

　第4章「帰納的証明プランを用いる証明手続き」は、前章の基本的な証明手続きの自動化を取り上げ、帰納的証明プランを作成することによって証明木を効率よく探索する手法を提案したものである。基本的な証明手続きをそのまま用いて証明木を探索すると、複数の推論規則が適用可能なので探索空間が巨大であるため、妥当な時間で答えを返すことが出来ない。本論文では、証明する論理式の中に現れる変数の再帰パターンと呼ばれるものを解析し、これから、証明木の言わば幹の部分をどのように作るかを示す帰納的証明プランを作成し、証明木を効率良く作り出すことが出来ることを確認している。

　第5章「補題の利用を組み込んだ証明手続き」は、既に証明されている論理式を、別の論理式の証明の途中で「補題」として利用するための推論規則を提案したものである。

　第6章「証明システムの実装とその実験的評価」は、前章までに提案された証明手続きを並列論理型言語KL1を用いて並列計算機マルチPSI上に実装した証明システムについてまとめたものである。そのインターフェイスと内部構成、実装技法について述べ、この証明システムを用いて中規模の証明木を自動的に作り上げることが出来ることを実験的に示し、その証明木のサイズや証明時間について報告している。

　第7章「ハードウェア検証への応用」は、Hornプログラムを用いてハードウェア回路を記述し、その論理的性質を証明することによって、ハードウェア設計の正しさを検証する方法について述べたものである。特に、本章では、算術演算を行なう加算器や乗算器について、回路に現れる空間的繰り返し構造を活かし、帰納法を用いることによって、任意のNビットの加算器や乗算器の機能的な正しさを検証できることを、前章で述べた証明システムを用いて実験的に示している。

　第8章「検討」は、第3章から第4章までに述べた証明手続きをさらに精緻化する方法について、また、論理型プログラムや関数型プログラムの論理的性質の帰納的証明について、従来行なわれてきた研究との関係、差異について論じたものである。

　第9章は「むすび」である。

　以上、これを要するに、本論文は、情報処理システムの論理的記述の検証の多くの応用の基礎となる、Hornプログラムの論理的性質の証明手続きについて検討し、帰納的証明プランの使用、補題の利用、並列化などを通して、その論理的性質を厳密に、かつ、自動的に証明することを可能ならしめることにより、この記述方法の適用の効果と範囲を拡大したもので、情報工学上、貢献する所、少なくない。

　よって、本論文は、博士(工学)の学位請求論文として合格と認められる。