高度な制約解析を可能にする自動証明装置

国立大学法人京都大学

京都府京都市左京区吉田本町

この技術でできること

制約を具体的な多項式として設定し、クレイグ補間を用いた解析を行う自動証明装置

相談したいこと

技術の特徴

この特許では、自動証明装置の新たなアプローチが示されています。証明対象に関連する制約を、0以上の多項式、0より大きい多項式、0に等しい多項式のいずれかを少なくとも一つ含む形で設定します。その後、ソルバーがこれらの制約を用いてクレイグ補間を表す多項式を生成し出力します。これにより、出力される解はプログラム検証や定理証明の処理に利用されます。また、複数の近似係数を求め、それらを予め定めた方法で選択し、試行多項式を生成する能力も持っています。試行多項式がクレイグ補間を表す多項式として成立するかを検証し、成立しない場合はエラーを生成し、所定の処理を実行します。これにより、より精度の高い解析と証明の自動化が可能となります。

AIによる特許活用案

おすすめ業界 ITソフトウェア開発ハードウェア設計

プログラム検証の自動化

この自動証明装置は、プログラムコードの検証を自動化するツールとして活用できます。特定の制約条件下でのプログラムの挙動を解析し、予期しないエラーやバグを事前に検出することが可能です。

続きの活用案は会員限定です

無料登録またはログイン後に、公開範囲に応じて確認できます。

参考情報

活用条件

サブスクリプション・未選択
権利譲渡・未選択
ライセンス契約・未選択

商品化・サービス化: ASK
実証実験: ASK
サンプル・プロトタイプ: ASK

掲載者による選択状態を表示しています。未選択や ASK は、利用不可を意味するものではありません。

権利概要

出願番号: 特願2017-137949
発明の名称: 自動証明装置、及びプログラム
出願人／権利者: 国立大学法人京都大学
住所: 京都府京都市左京区吉田本町
公開番号: 特開2019-020966
登録番号: 特許第6910228号

登録情報の修正申請