文献

J-GLOBAL ID：202002265730280062   整理番号：20A1634592

ローカルによる代数テキストの構造の探索【JST・京大機械翻訳】

Exploring the Structure of an Algebra Text with Locales

著者 (1件)： Ballarin Clemens (Karlsruhe, Germany)
資料名： Journal of Automated Reasoning  (Journal of Automated Reasoning)
巻： 64  号： 6  ページ： 1093-1121  発行年： 2020年 
JST資料番号： D0269E  ISSN： 0168-7433  CODEN： JAREEW  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 局所,定理証明器Isabelleのモジュールシステムを設計して,抽象代数における開発を忠実かつ簡潔に表現することができた。これらの目標を事例研究を通して評価した。構造的に挑戦的な代数テキストブック,Jacobsonの基本代数の部分を定式化した。形式化の鍵となる部分を,より詳細に提示した。定性的および定量的展望の両方からの作業の解析は,設計目標が満たされていることを証明した。特に,「ペンと紙」テキストに対する形式の比率は,さらに書籍に進むと増加しなかった。また,この解析は,使用のパターンを含む局所に関する指針をもたらし,それを同定,記述した。Copyright Springer Nature B.V. 2019 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 定理証明 ,  *事例研究 ,  定式化

著者キーワード (6件)： 抽象代数 ,  事例研究 ,  Isabelle ,  地方 ,  モジュールシステム ,  定理証明器

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

タイトルに関連する用語 (2件)： 代数 ,  探索