TOP > 国内特許検索 > 自動証明装置、及びプログラム

自動証明装置、及びプログラム

国内特許コード P200016800
整理番号 5771
掲載日 2020年5月8日
出願番号 特願2017-137949
公開番号 特開2019-020966
出願日 平成29年7月14日(2017.7.14)
公開日 平成31年2月7日(2019.2.7)
発明者
  • 蓮尾 一郎
  • 奥殿 貴仁
  • 木戸 肩吾
  • 末永 幸平
  • 小島 健介
  • 西田 雄気
出願人
  • 国立大学法人東京大学
  • 国立大学法人京都大学
発明の名称 自動証明装置、及びプログラム
発明の概要 【課題】得られた補間に対応する現実の証明対象の解釈を容易化できる自動証明装置及びプログラムを提供する。
【解決手段】与えられた証明対象に係るクレイグ補間を表す多項式を生成して出力するソルバーからの入力を受け入れる、当該項式に含まれる係数の比を、整数の比であり、各係数に対応する値がより小さい値となるよう近似した近似係数を求め、当該求められた近似係数のうちから、予め定めた方法で決定された順に、近似係数を選択して、受け入れた多項式の係数を当該選択した近似係数に置き換えた試行多項式を生成し、当該試行多項式が、前記クレイグ補間を表す多項式として成立するかを検証する自動証明装置である。
【選択図】図1
従来技術、競合技術の概要

近年、大規模集積回路(LSI)等の、ハードウェアの設計や検証、ソフトウェアプログラムの検証等において、人為的介入なしに自動で推論を行う自動証明装置の利用が検討されている。例えば、非特許文献2には、ハードウェア設計を、クレイグ補間を用いた方法で検証を行うことで、検証可能な対象を広げることができることが開示されている。

こうした研究を受けて、与えられた証明対象に係るクレイグ補間を表す多項式を生成して出力するソルバーが開発されている(例えば非特許文献1)。このようなソルバーにおいては、多項式の係数が、数値解析により得られているので、一般に簡潔な整数比としては表現されない。また、当該係数には数値誤差を含む。

産業上の利用分野

本発明は、自動証明装置、及びプログラムに関する。

特許請求の範囲 【請求項1】
与えられた証明対象に係るクレイグ補間を表す多項式を生成して出力するソルバーからの入力を受け入れる手段と、
前記受け入れた多項式に含まれる係数の比が、整数の比となり、かつ各係数に対応する値がより小さい値となるよう近似した近似係数を、複数求める係数演算手段と、
前記複数求められた近似係数のうちから、予め定めた方法で決定された順に近似係数を選択し、前記受け入れた多項式の係数を当該選択した近似係数に置き換えた試行多項式を生成し、当該試行多項式が、前記クレイグ補間を表す多項式として成立するかを検証する検証手段と、
前記検証により、前記求めたいずれかの近似係数に基づく前記試行多項式が、前記クレイグ補間を表す多項式として成立すると、前記検証手段により判断されたときに、当該近似係数を、解として生成する生成手段と、
を含み、
前記生成手段は、前記求めたいずれかの近似係数に基づく前記試行多項式が、いずれも前記クレイグ補間を表す多項式として成立しないとして前記検証手段により判断されたときには、エラーが発生したものとして所定の処理を実行する、
自動証明装置。

【請求項2】
請求項1記載の自動証明装置であって、
前記ソルバーは、前記証明対象に係る制約が、
任意の変数値に対して
0以上である多項式f、
0より大である多項式g、
0に等しい多項式h
のいずれかを少なくとも一つ含んで設定され、
一対の制約T,T′のクレイグ補間を表す多項式を生成して出力するソルバーである自動証明装置。

【請求項3】
請求項1または2に記載の自動証明装置であって、
前記出力される解が、プログラム検証または定理証明の処理に供される自動証明装置。

【請求項4】
請求項1に記載の自動証明装置であって、
前記ソルバーは、前記証明対象に係る制約が、
任意の変数値に対して
0以上である多項式f、
0に等しくない多項式g、
0に等しい多項式h
のいずれかを少なくとも一つ含んで設定され、
一対の制約T,T′のクレイグ補間を表す多項式を生成して出力するソルバーである自動証明装置。

【請求項5】
コンピュータを、
与えられた証明対象に係るクレイグ補間を表す多項式を生成して出力するソルバーからの入力を受け入れる手段と、
前記受け入れた多項式に含まれる係数の比が、整数の比となり、かつ各係数に対応する値がより小さい値となるよう近似した近似係数を、複数求める係数演算手段と、
前記複数求められた近似係数のうちから、予め定めた方法で決定された順に近似係数を選択し、前記受け入れた多項式の係数を当該選択した近似係数に置き換えた試行多項式を生成し、当該試行多項式が、前記クレイグ補間を表す多項式として成立するかを検証する検証手段と、
前記検証により、前記求めたいずれかの近似係数に基づく前記試行多項式が、前記クレイグ補間を表す多項式として成立すると、前記検証手段により判断されたときに、当該近似係数を解として生成し、前記求めたいずれかの近似係数に基づく前記試行多項式が、いずれも前記クレイグ補間を表す多項式として成立しないとして前記検証手段により判断されたときには、エラーが発生したものとして所定の処理を実行する生成手段と、
として機能させるプログラム。
国際特許分類(IPC)
Fターム
画像

※ 画像をクリックすると拡大します。

JP2017137949thum.jpg
出願権利状態 公開
ライセンスをご希望の方、特許の内容に興味を持たれた方は、下記までご連絡ください。


PAGE TOP

close
close
close
close
close
close
close