离散外微分与计算电磁学

计算电磁学的核心之一是数值求解Maxwell方程组.适当的离散方式是保证结果能真实反映物理现象的关键.为了在离散的过程中保持该方程组的几何性质,我们建立了基于棱柱网格的系数为R的格点规范理论,其离散曲率满足相应的Bianchi恒等式.通过适当定义离散微分形式之间的内积和棱柱网格上的Hodge星算子,我们由离散变分导出源方程和连续性方程,和Bianchi恒等式一起称为真空中的离散Maxwell方程组.这组方程是内蕴的,并具有规范不变性.     

图表追踪的一种机器实现方法

交换图表追踪法是同调代数中一种重要的证明方法.本文提出了一种基于前推的交换图表追踪的机器实现方法,它可以证明同调代数中一系列基于交换图的定理.该方法从定理的结论出发,通过构造辅助元素以及对辅助元素进行推导,能在有限步内给出定理的证明.本文提出的前推方法已经在Java开发平台上实现,同调代数中的五引理、九引理、蛇引理等的证明都可以由我们的程序自动产生.     

基于指标形式张量的微分几何定理机器证明

提出了一个基于指标形式张量的微分几何定理的机器证明算法.该算法将微分几何定理转化成带指标的张量多项式的计算问题,然后通过利用重写规则,挖掘等价条件和分次选取条件等方法大大减少了这个多项式系统的方程个数.再利用这个多项式系统本身和关于哑元的方程三角化这个多项式系统,将所得到的首项代入结论, 从而得到了该定理的机器证明.该算法不仅能够证明基于指标形式张量的微分几何定理,也可以用于张量方程的求解.     

Numerical Simulation of Electromagnetic Waves Scattering by Discrete Exterior Calculus

We show how to construct discrete Maxwell equations by discrete exterior calculus. The new scheme has many virtues compared to the traditional Yee＇s scheme： it is a multisymplectic scheme and keeps geometric properties. Moreover, it can be applied on triangular mesh and thus is more adaptive to handle domains with irregular shapes. We have implemented this scheme on a Java platform successfully and our experimental results show that this scheme works well.