[拼音]：gongshi tuiyan
[外文]：formula manipulation
由计算机自动推演数学公式的技术，是人工智能的一个应用领域，又称计算机代数。运用公式推演技术能使人们从手工的繁琐和容易出错的符号演算和推理中摆脱出来。(3+4)2=49,这是数值计算;而(a+b)2=a2+2ab+b2就是公式推演，这时被计算对象是符号式，结果也是符号式。
公式推演的研究始于1953年。1966年美国计算机协会成立符号和代数推演专业组(SIGSAM)，并出版了这方面的刊物《ACM SIGSAM Bulletin》。
公式推演的内容包括数学式的化简、多项式四则运算、求最大公因式、因式分解、有理式的各种运算、符号矩阵、行列式、张量运算、线性和非线性方程组的符号解、符号微分、不定积分、常微分方程和数理方程的解析解、各种特殊函数的推导和函数的级数展开等。公式推演的研究分为算法、系统和应用三个方面。
算法针对各种公式推演对象，改进已有算法或提出新算法。例如求两个多项式的最大公因式的算法、因式分解算法、求有理函数的不定积分的算法等。
系统目前世界上已有60多个公式推演系统，可分通用系统和专用系统两种类型。如美国麻省理工学院研制的MACSYMA,是著名的通用公式推演系统，也是求解数学问题的大型知识型系统或专家系统；ASHMEDAI则是量子电动力学问题的专用公式推演系统。muMATH是适于在微型机上运行的公式推演系统。
MACSYMA是交互式计算机程序系统,它以符号形式输入和输出，并可调用多种数值计算的子程序库和绘图程序包,因此公式推演功能很强。这个系统已与美国高级研究计划局的通信网络即阿帕网(ARPA网)联网。MACSYMA的化简程序能自动地根据一组规则对数学式进行化简，这类规则的例子如
在进行数学式化简时,MACSYMA还利用语义模式匹配程序。这个程序使用关于运算符和常数的知识发现非语法的匹配。例如ax2+bx+c（其中a、b、c都是与x无关的模式变元）这一模式能与2x2+1、(x+3)2、3x2+5x+2等表达式匹配，但不能与 2x2 + x sinx+1匹配。
表达式尺寸大小(即所含项数多少)是衡量表达式简单程度的一个有用指标。根据最小表达式的思想，MAC-SYMA采用了一个面向搜索的爬山程序（算法），它对数学表达式的化简如下例：
已知条件：K2+L2=1N2-M2=1
原始表达式：K2N2+K2M2N2-K2L2N2-K2L2M2N2
中间表达式：K4M2N2+K4N2（原始式代换L而得）
最终表达式：K4N4（中间式代换M而得）
在某些问题中为便于化简，数学式中的符号在取值范围或其他性质方面受到一定限制,为此MACSYMA设置了一个关系数据库，以语义网络形式存放关于符号的事实。例如用户通过说明命令规定符号 m的值限为整数，那么化简程序能将
简化为零。又如用户通过假设命令设定x ≤y，y≤z和z ≤x，那么MACSYMA便能推出x=y=z。
MACSYMA有一个自动符号积分程序,它使用启发式技术。积分程序将被积函数分为11类，相应就有11个积分功能模块。积分程序根据被积函数中子式的启示，将它交给相应的积分功能块去处理。例如被积函数含有子式sin(2x),则用三角函数的积分功能块去处理。遇到积不出的情况，符号积分程序会给出报告。
为了便利用户,MACSYMA提供了联机支援程序和用户培训程序（智能化计算机辅助数学程序）。
应用公式推演技术已成功地用于天体力学、相对论、高能物理、等离子体物理、量子电动力学、流体力学、数学、化学、电路网络理论、排队论等科学领域,也成功地用于船体设计、直升机设计、电子显微镜设计等工程技术问题。MACSYMA系统已移交美国的能源研究与开发局、国家航空航天局、全国卫生研究院和海军实验室使用。
在求解一组描述天体运动规律（包括行星、人造卫星、太空站等）的微分方程时，通常采用逐次逼近法。解的形式是以小参数（如轨道的偏心率）表示的幂级数。从1847年起法国天文学家 G.-E.德洛内为研究月球运动公式花了20年时间，而1970年美国西雅图波音实验室的A.德普瑞特等人用公式推演和数值计算相结合的技术在计算机上只用了20小时就重新算出德洛内的公式并纠正了三处错误。
R.P.费因曼用他建立的费因曼图来研究量子电动力学中电子和光子间相互作用的微扰理论。对电子异常磁矩进行准确到六阶微量的修正计算，需要分析72张费因曼图，涉及大量繁琐的积分运算。应用公式推演技术可将积分结果先用符号形式表示, 然后再进行数值计算， 能大大提高计算效率。在 UNIVAC1108 机上运行专用的ASHMEDAI系统对一张复杂的费因曼图进行分析仅需要35分钟。