首页--数理科学和化学论文--数学论文--代数、数论、组合理论论文--抽象代数(近世代数)论文

基于交互式定理证明工具Coq构建的近世代数理论--特例研究:主理想环因式分解定理的机器证明

摘要第4-5页
ABSTRACT第5-6页
第一章 绪论第10-16页
    1.1 形式化方法第10-11页
    1.2 Coq简介第11-12页
    1.3 近世代数简介第12-13页
    1.4 主理想环的因式分解定理第13页
    1.5 文章结构安排第13-16页
第二章 Coq的基础语法第16-28页
    2.1 Coq中项的基础语法第16-20页
        2.1.1 类型第16-18页
        2.1.2 声明和定义第18-20页
    2.2 Coq中命题的描述第20-21页
        2.2.1 Coq中的量词第20页
        2.2.2 Coq中的命题定义第20-21页
    2.3 Coq中常用的基础命令第21-28页
第三章 基于Coq的基础定义和性质第28-50页
    3.1 近世代数中的基础概念第28-35页
    3.2 近世代数中的群论第35-39页
    3.3 近世代数中的环论第39-47页
    3.4 近世代数中的域论第47-50页
第四章 主理想环因式分解定理的机器证明第50-78页
    4.1 整环的因式分解相关的定义第50-54页
    4.2 主理想环因式分解定理的证明第54-78页
        4.2.1 预备定理1的证明第54-63页
        4.2.2 预备定理2的证明第63-66页
        4.2.3 性质1的证明第66-72页
        4.2.4 性质2的证明第72-75页
        4.2.5 主理想环因式分解定理的证明第75-78页
第五章 总结及展望第78-82页
    5.1 研究总结第78-79页
    5.2 研究不足第79-80页
    5.3 研究展望第80-82页
参考文献第82-86页
附录第86-96页
    附录1 剩余类环定理的Coq证明第86-90页
    附录2 唯一分解定理的Coq证明第90-96页
致谢第96-98页
攻读学位期间取得的研究成果第98页

论文共98页,点击 下载论文
上一篇:二阶椭圆混合问题和Stokes问题的有限元逼近
下一篇:解析函数q差分的值分布性质