国立大学法人京都大学
高度な制約解析を可能にする自動証明装置
国立大学法人京都大学
高度な制約解析を可能にする自動証明装置
この特許では、自動証明装置の新たなアプローチが示されています。証明対象に関連する制約を、0以上の多項式、0より大きい多項式、0に等しい多項式のいずれかを少なくとも一つ含む形で設定します。その後、ソルバーがこれらの制約を用いてクレイグ補間を表す多項式を生成し出力します。これにより、出力される解はプログラム検証や定理証明の処理に利用されます。また、複数の近似係数を求め、それらを予め定めた方法で選択し、試行多項式を生成する能力も持っています。試行多項式がクレイグ補間を表す多項式として成立するかを検証し、成立しない場合はエラーを生成し、所定の処理を実行します。これにより、より精度の高い解析と証明の自動化が可能となります。
つまりは、制約を具体的な多項式として設定し、クレイグ補間を用いた解析を行う自動証明装置
AIによる特許活用案
おすすめ業界 ITソフトウェア開発ハードウェア設計
- プログラム検証の自動化
- ハードウェア設計の効率化
- 教育・研究の支援ツールとして
この自動証明装置は、プログラムコードの検証を自動化するツールとして活用できます。特定の制約条件下でのプログラムの挙動を解析し、予期しないエラーやバグを事前に検出することが可能です。
大規模集積回路（LSI）などのハードウェア設計において、この自動証明装置を活用することで設計の効率化が図れます。設計の過程で生じるさまざまな制約条件を解析し、設計の最適化を支援します。
教育や研究の場では、新たな理論や概念の証明が重要な役割を果たします。この自動証明装置は、そのような証明作業を効率化し、新たな発見を加速することができます。また、学生が新たな理論を学ぶ際の教材としても活用できます。
活用条件
- サブスク
- 譲渡
- ライセンス
商品化・サービス化 実証実験 サンプル・プロトタイプ
特許評価書
- 権利概要
| 出願番号 | 特願2017-137949 |
| 発明の名称 | 自動証明装置、及びプログラム |
| 出願人/権利者 | 国立大学法人京都大学 |
| 公開番号 | 特開2019-020966 |
| 登録番号 | 特許第0006910228号 |
- サブスク
- 譲渡
- ライセンス
準備中です