教学课程资源库 更多>>

关键词： 近世代数   高等代数   群   环   域  

摘要： 本文结合近世代数的教学实践经验,通过具体的例子介绍了高等代数在群、环和域等近世代数问题中的应用。应用高等代数,不但能化抽象为具体,而且能开拓解题思路,对学生深入理解近世代数有积极作用。

关键词： 近世代数   线性代数   群  

摘要： 近世代数一直都是本科数学专业学生的一大拦路虎,很多学生会觉得困难、吃力.如何在一开始的群论学习中让学生觉得有趣、有用,从而产生学习动力,显得至关重要.本文根据近年来的教学实践,谈一谈在群论教学中的几点体会.

关键词： 近世代数   教学改革   教学方法   课堂教学  

摘要： 针对贵州民族大学数学与应用数学、信息与计算科学两个专业近世代数课程课堂教学中存在的问题,结合自身的教学实践,从教材、教学内容、教学方法、考核方式等方面,给出了近世代数课程教学改革的几点建议。

关键词： 近世代数   研讨式教学   抽象性   习题课   考核方式  

摘要： 近世代数是数学专业的重要课程,现已渗透各个科学领域,特别是在编码、密码等方面的应用更是十分广泛。文章主要探讨了近世代数课程的实用教学方法,以增强教学效果,进一步提升学生运用数学的能力。

关键词： Coq   机器证明   近世代数   群   同态  

摘要： 人工智能是作为新一轮科技革命和产业变革的重要驱动力,是引领未来的战略性技术,已正式上升为国家战略。而人工智能中一个非常重要分支就是自动推理,自动推理的大量工作都集中在定理机器证明中。定理机器证明是指使用计算机证明定理的成立,即把人证明定理的过程,通过一套符号体系加以形式化,变成一系列在计算机上自动实现的符号计算的过程[1],它是人工智能近代主攻的课题之一。Coq是一个基于归纳构造演算的交互式定理证明工具[2],它使用类型对需要验证的程序或命题进行描述和证明,非常适合证明需要严格符合规范的程序。目前,在国内外的定理机器证明领域,Coq是主流的辅助证明工具之一,它有着强大的数学模型基础和良好的扩展性,并拥有完整的工具集[3],在推理和编程方面,表现出强大的表达能力。序结构、代数结构、拓扑结构是数学的三大基本母结构,这三大母结构的交融促进了数学的纵深发展。代数结构包括群、环、域三大结构[4-6],其中群是环和域的基础,群在数学领域有着举足轻重的地位,在其他学科也有广泛的应用。数学定理的机器证明是数学可靠性和严谨性的体现,它连通了计算机领域和数学领域,通过机器验证过的定理是完全可信的。对群论实现形式化是对其进行验证的过程,在数学定理的机器证明领域具有深刻意义。本文以张禾瑞教授的著作《近世代数基础》作为理论依据,基于交互式定理证明工具Coq,构建了群论体系的形式化系统。本文从近世代数的基本概念出发,给出了集合、映射、代数运算、关系等概念的形式化定义,然后给集合加上运算,定义出群的概念。接着讨论了一些特殊的群,并定义出子群,在不变子群的基础上讨论了群的同态、不变子群和商群,最后针对群论中的一些重要定理给出了形式化证明。本文的创新点在于利用Coq实现了以上定义的形式化描述以及定理的严谨证明,群论的形式化不仅验证了群论体系的严谨性与可靠性,更是数学在人工智能领域的一个成功的案例。

关键词： 带余除法   环   多项式   高等代数   同余类  

摘要： 带余除法在代数数学中占据着重要的地位，本科阶段唯一接触的两门关于代数数学的课程就是高等代数和近世代数。无论是高等代数还是近世代数，都存在带余除法定理。二者之间具有一定的联系，也存在着一些不同.学习了近世代数后，为“多项式的因式分解”提供了新的思路。文章就高等代数与近世代数中的带余除法定理进行了简单的比较和分析，同时对比了环与矩阵上的运算规律，思考整系数多项式环中的因式分解，加深对于知识的理解和认识。

关键词： 形式化数学   定理机器证明   近世代数   环和域   Coq  

摘要： 人工智能技术是国家目前重大科技发展战略之一,是计算机科学发展中非常重要的一个支系。随着现代社会计算机化、智能化程度的日渐提高,与计算机相关的各种系统故障往往会造成现代社会的巨大经济损失,更有甚者,会危及到人类的生命安全,因此夯实人工智能基础理论对现代智能化社会来说尤为重要。定理机器证明能够对计算机程序建立更为严格的正确性,从而奠定系统的高可信性,是人工智能基础理论的深刻体现。交互式定理证明工具Coq是进行数学定理机器证明的有力工具。法国布尔巴基学派的序结构,代数结构,拓扑结构三大结构组成了现代数学的基础。这三大结构相互交融,形成现代数学的主体内容。利用计算机证明辅助工具Coq,可以完整构建这三大结构的形式化系统。由于代数元素的通用性,许多学科把代数系统当作其研究的基本工具和语言。代数系统(带有运算的集合)是代数研究的基本对象。近世代数是研究代数系统的学科,在数学的其他分支和自然科学的许多部门里都有重要应用。在现代科学中,它的一些成果更被直接用于某些新兴技术的研究,如密码学等。环和域是近世代数中最基本的代数系统。本文基于交互式定理证明辅助工具Coq,实现近世代数中环和域理论基本框架的形式化。主要工作如下:(1)利用交互式定理证明辅助工具Coq,从集合、映射等数学基础概念出发,实现构建代数系统所需基本概念的形式化。这些基础概念的形式化具有高可复用性,可用于构建多种代数系统,还可用于构建需要用到这些概念的其他数学理论比如序结构,拓扑结构,微积分等。(2)实现近世代数中环和域两种代数系统的形式化,并完成这两种代数系统基本性质的定理证明。(3)环同态基本定理是近世代数中的重要内容,是比较两个代数系统最有效的工具,可以利用这一定理将抽象代数系统的问题具体化。本文利用交互式定理证明工具Coq,给出了环同态基本定理的机器证明。该定理的所有证明过程由Coq给出形式化描述,体现了基于Coq的数学定理机器证明具有可读性,智能性的特点,证明过程规范,严谨,可靠。

关键词： 近世代数   现代手段   效率   兴趣  

摘要： 探讨如何加强学生对抽象的代数概念和定理的理解,激发学生的学习兴趣,增强学生的自主学习能力以及提高课堂的教学效率等,从教学内容、教学方法和教学手段三个方面提出几点改进意见。

关键词： 同构思想   线性空间   群   环  

摘要： 在高等代数和近世代数课程的教学中,需要设计恰当的例题和习题来帮助学生理解一些抽象的概念.在经典的代数类教材中,会发现一些设计精巧而又富有趣味性的习题和例题.一个自然的问题是,这些例题和习题是如何设计出来的?本文通过四个例子展示了同构思想在这些题目设计中的重要作用.