自動化定理證明 agda2中的一个证明例子 自動化定理證明(Automated theorem proving,簡稱ATP)目前是自动推理(Automated reasoning,簡稱AR)体系中发展最好的部分,它的目的是为使用电子计算机程序来进行数学定理的证明。对于不同的公理系统,它能够推论出一个定理在此系统下是正确的,还是不可证明的,或者错误的。 參考[编辑] 電腦協助證明 查论编应用数学运算数学 算法 算法设计 算法分析 自動機理論 自动化定理证明 编码理论 计算几何 约束满足 约束编程 计算机逻辑 密码学 信息论 计算统计学 离散数学 计算机代数 计算数论 组合数学 图论 离散几何学 数学分析 逼近理论 克利福德分析(英语:Clifford analysis) 克利福德代数 微分方程 常微分方程 偏微分方程 随机微分方程 微分几何 微分形式 规范理论 几何分析 动力系统 混沌理论 控制理论 泛函分析 算子代数 算子理论 调和分析 傅里叶分析 多重线性代数 外代数 几何代数 张量 向量代数 多元微积分 外微积分 几何微积分(英语:Geometric calculus) 张量微积分(英语:Tensor calculus) 向量微积分 数值分析 数值线性代数 常微分方程数值方法 偏微分方程数值方法 变分法 概率论 概率分布(随机变量) 随机过程 / 随机分析 泛函积分 马利阿温微积分(英语:Malliavin calculus) 数学物理 分析力学 拉格朗日力学 哈密顿力学 场论 经典场论 共形场论 有效场论 规范场论 量子场论 统计场论 拓扑量子场论 摄动理论 微扰理论 (量子力学) 位势论 弦理论 玻色弦理论 拓扑弦论 超对称 超对称量子力学(英语:Supersymmetric quantum mechanics) 随机力学超对称理论(英语:Supersymmetric theory of stochastic dynamics) 代数结构 物理空间代数 路径积分表述 泊松代数 量子群 重整化群 粒子物理与表示论(英语:Particle physics and representation theory) 时空代数 超代数 超对称代数(英语:Supersymmetry algebra) 决策论 博弈论 运筹学 最优化 社会选择理论 统计学 数理经济学 数理金融学 其他应用 数理生物学 数学化学(英语:Mathematical chemistry) 数学心理学 数理社会学 相关领域 数学 数学软件 社会组织 工业与应用数学学会 日本应用数理学会(英语:Japan Society for Industrial and Applied Mathematics) 法国应用与工业数学学会(英语:Société de Mathématiques Appliquées et Industrielles) 国际工业与应用数学理事会(英语:International Council for Industrial and Applied Mathematics) 分类 话题 这是一篇关于数学的小作品。你可以通过编辑或修订扩充其内容。查论编