文献

J-GLOBAL ID：202202218272744324   整理番号：22A0931056

二重ワード演算の形式化,および「二重ワード算術の基本ビルディングブロックに対するタイトおよび厳密な誤差限界」についてのコメント【JST・京大機械翻訳】

Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic”

著者 (2件)： Muller Jean-Michel (CNRS, LIP, Universite de Lyon, Lyon Cedex 07, France) ,  Rideau Laurence (Inria Sophia Antipolis, Universite Cote d’Azur, Sophia Antipolis Cedex, France)
資料名： ACM Transactions on Mathematical Software  (ACM Transactions on Mathematical Software)
巻： 48  号： 1  ページ： 1-24  発行年： 2022年 
JST資料番号： D0669A  ISSN： 0098-3500  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 最近,二重語数(古典的,いくつかの新しい)を操作するためのアルゴリズムの完全なセットを,[16]で分析した。Coq証明支援を用いて,本論文で与えられたすべての定理を形式的に証明した。形式的証明作業は著者らを導いた。(i)いくつかのオリジナル論文証明の誤り(しかし,アルゴリズムの妥当性を妨げない)は,(ii)いくつかの誤差限界を著しく改善し,(iii)丸めモードをわずかに変更するならば,それらがまだ有効であることを示すことによって,いくつかの結果を一般化する。結果は,[16]で提示されたアルゴリズムが,高い信頼度で使用でき,それらの幾つかが以前に信じられるものよりさらに正確であるということであった。これは,形式的証明がコンピュータ演算にもたらすことができることを示す:単なる(非常に有用な)検証,補正,および既に知られている結果の圧密化を超えて,それは新しい特性を見つけるのを助けることができる。すべての形式的証明は自由に利用可能である。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 圧密 ,  アルゴリズム ,  信頼度 ,  証明 ,  *演算 ,  浮動小数点演算 ,  定理 ,  形式 ,  検証 ,  *単語 ,  コンピュータ
準シソーラス用語： *ビルディングブロック ,  *算数 ,  誤差限界 , 【Automatic Indexing@JST】

著者キーワード (6件)： 浮動小数点演算 ,  ダブルワード演算 ,  二重演算 ,  形式化 ,  証明アシスタント ,  Coq

分類 (1件)： 計算理論  (JB02000A)

タイトルに関連する用語 (6件)： ワード ,  形式化 ,  算術 ,  ビルディングブロック ,  誤差限界 ,  コメント