教学课程资源库 更多>>

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

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

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

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

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

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

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

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

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

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

关键词： 近世代数   教学改革   探讨  

摘要： 近世代数是大学数学专业比较抽象的一门专业必修课.从教学内容、教学方法和教学手段等方面给出如何提高课堂教学效果的几点体会.

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

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

关键词： 二元运算   近世代数   群   映射  

摘要： 近世代数中群概念抽象、概括性高,不易理解,从映射的要素来理解和认识群定义中的运算和规则。

关键词： 探究式教学   群   置换   子群的陪集  

摘要： 针对近世代数内容抽象的特点,采用探究式教学法引导学生从实例出发,探究出定义、定理的内容;介绍了一些探究式学习的教学设计方法,包括由具体到抽象教学法、类比教学法、趣味教学法、几何直观教学法等;探究式教学法强调了学生的主体性原则,表现为学生能够主动建构新知识,成为定义、定理的发现者.

关键词： 环论   群   代数运算   近世代数  

摘要： 环是群在定义上的进一步延伸,但环又比群多了一重代数运算,文章首先对环的定义进行详细阐述,之后再对环论中若干典型问题进行探究,并尽可能给出详细的解法。