文献

J-GLOBAL ID：201802257973355394   整理番号：18A1061321

高階差分にもとづくループ停止性証明方法

Method for Proving Loop Termination Using Higher Order Differentials

著者 (1件)： 千代英一郎 (成蹊大学理工学部)
資料名： コンピュータソフトウェア  (Computer Software)
巻： 35  号： 2  ページ： 2_109-2_115(J-STAGE)  発行年： 2018年 
JST資料番号： Y0628A  ISSN： 0289-6540  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 本稿では,高階差分の概念を導入することで,ある式の値がループの繰り返しのなかで「将来的に常に正になる(あるいは負となる)」という時相的な情報を利用してループの停止性証明を行う方法を提案する.単なる差分だけではなく,2階以上の差分(高階差分)を考慮することで,標準的なランキング関数にもとづくアプローチでは取扱いの面倒な,連続する複数回の繰り返しにまたがる式の値の変化を直接的に扱うことが可能となる.本稿で示す定理にもとづく証明は従来と同じ1階述語論理の範囲内で行えるため,充足可能性判定問題に帰着させることでSMTソルバを用いた効率的な判定が可能である.(著者抄録)

シソーラス用語： *定理証明 ,  *プログラム理論 ,  ループ ,  *計算機プログラム ,  時間論理 ,  経時変化 ,  *充足可能性問題
準シソーラス用語： *高階差分 ,  時相論理

分類 (3件)： 計算理論  (JB02000A) ,  計算機システム開発  (JD02010R) ,  論理代数  (JB03000H)

タイトルに関連する用語 (4件)： 差分 ,  ループ ,  停止性 ,  証明