特許
J-GLOBAL ID:201903014390031398

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

発明者:
出願人/特許権者:
代理人 (1件): 竹居 信利
公報種別:公開公報
出願番号(国際出願番号):特願2017-137949
公開番号(公開出願番号):特開2019-020966
出願日: 2017年07月14日
公開日(公表日): 2019年02月07日
要約:
【課題】得られた補間に対応する現実の証明対象の解釈を容易化できる自動証明装置及びプログラムを提供する。【解決手段】与えられた証明対象に係るクレイグ補間を表す多項式を生成して出力するソルバーからの入力を受け入れる、当該項式に含まれる係数の比を、整数の比であり、各係数に対応する値がより小さい値となるよう近似した近似係数を求め、当該求められた近似係数のうちから、予め定めた方法で決定された順に、近似係数を選択して、受け入れた多項式の係数を当該選択した近似係数に置き換えた試行多項式を生成し、当該試行多項式が、前記クレイグ補間を表す多項式として成立するかを検証する自動証明装置である。【選択図】図1
請求項(抜粋):
与えられた証明対象に係るクレイグ補間を表す多項式を生成して出力するソルバーからの入力を受け入れる手段と、 前記受け入れた多項式に含まれる係数の比が、整数の比となり、かつ各係数に対応する値がより小さい値となるよう近似した近似係数を、複数求める係数演算手段と、 前記複数求められた近似係数のうちから、予め定めた方法で決定された順に近似係数を選択し、前記受け入れた多項式の係数を当該選択した近似係数に置き換えた試行多項式を生成し、当該試行多項式が、前記クレイグ補間を表す多項式として成立するかを検証する検証手段と、 前記検証により、前記求めたいずれかの近似係数に基づく前記試行多項式が、前記クレイグ補間を表す多項式として成立すると、前記検証手段により判断されたときに、当該近似係数を、解として生成する生成手段と、 を含み、 前記生成手段は、前記求めたいずれかの近似係数に基づく前記試行多項式が、いずれも前記クレイグ補間を表す多項式として成立しないとして前記検証手段により判断されたときには、エラーが発生したものとして所定の処理を実行する、 自動証明装置。
IPC (1件):
G06F 17/17
FI (1件):
G06F17/17
Fターム (1件):
5B056BB52

前のページに戻る