| 研究実績の概要 |
一般的帰納的定義の条件で次の(1)(2)を満たすものを発見し、その性質を証明する研究を行った。(1) 記号ヒープ体系にその条件下の一般的帰納的定義を追加しても、エンテイルメントの真偽が決定可能である, (2) リストセグメントなどのよく使用される基本的なデータ構造が記述できる. 本研究の実用的な意義は、メモリーエラーを自動定理証明により検証する方法に対して、リストセグメントのようなよく使われる基本的なデータ構造を扱うプログラムを対話的入力なしに全自動で検証できる方法をはじめて与えることである。
平成28年度の実績は次のようである。前年度の成果を拡張し、一般的帰納的定義を算術を含む体系に拡張した場合の充足可能性判定が決定可能であることを証明した.
|
