定理机械化证明的数值并行法及单点例证法原理概述被引量：9

原文传递

导出

摘要本文浅近地介绍以检验数值实例为基本手段的两种方法——洪加威提出单点例证法和张景中.杨路提出的数值并行法以及这两种方法与吴文俊数学机械化理论的关系.

作者张景中杨路

机构地区中科院成都分院数理科学研究室

出处《数学的实践与认识》 CSCD 北大核心 1989年第1期34-43,共10页 Mathematics in Practice and Theory

关键词数值并行法单点例证定理机械证明

参考文献4

1Yong-BinLi,WuLiu],Xiao-LinXiang.Geometry Theorem Proving by Decomposing Polynomial System into Strong Regular Sets[J].Journal of Computer Science & Technology,2004,19(6):820-827. 被引量：1
2张景中,杨路,侯晓荣.代数方程组相关性的一个判准及其在定理机器证明中的应用[J].中国科学（A辑）,1993,23(10):1036-1042. 被引量：9
3刘儒英.不可约圈并的补图的色唯一性[J].应用数学,1994,7(2):200-205. 被引量：12
4张景中,杨路,高小山,周咸青.几何定理可读证明的自动生成[J].计算机学报,1995,18(5):380-393. 被引量：22
5张景中,杨路,侯晓荣.几何定理机器证明的结式矩阵法[J].系统科学与数学,1995,15(1):10-15. 被引量：11
6张景中,杨路,侯晓荣.几何定理机器证明的WE完全方法[J].系统科学与数学,1995,15(3):200-207. 被引量：11
7张景中,高小山,周咸青.基于前推法的几何信息搜索系统[J].计算机学报,1996,19(10):721-727. 被引量：34
8郭知熠李永洁.关于圈并的补图的色唯一性[J].科学通报,1988,3:1676-1676.
9Chou S C，1989年
10邓来克，科学通报，1988年，24期，1851页

1徐茜.双向推理系统在初等几何自动解题中的实现[J].计算机应用研究,2004,21(11):232-234. 被引量：3
2Yong-BinLi,WuLiu],Xiao-LinXiang.Geometry Theorem Proving by Decomposing Polynomial System into Strong Regular Sets[J].Journal of Computer Science & Technology,2004,19(6):820-827. 被引量：1
3俞健.从中国古代数学思想到数学机械化现状[J].广州广播电视大学学报,2005,5(1):44-47.
4符红光,钟秀琴,曾振柄.三角函数表达式的计算机自动化简[J].计算机学报,2006,29(10):1869-1875. 被引量：1
5汤晓凌.集合论等式型定理机器证明系统的研究与开发[J].计算机工程与设计,2006,27(22):4378-4382.
6张景中.从数学难学谈起[J].世界科技研究与发展,1996,18(2):20-29. 被引量：26
7郭四稳.基于用户自添加规则的自动推理程序[J].计算机应用与软件,2007,24(9):48-50. 被引量：5
8张景中.几何定理机器证明20年[J].科学通报,1997,42(21):2248-2259. 被引量：7
9罗慧敏.基于消点法的几何自动推理系统实现[J].计算机应用,2008,28(11):2984-2986. 被引量：5
10潘斌,郭红霞.MPI环境下的几何定理并行自动推理[J].电子科技大学学报,2008,37(6):908-912.

数学的实践与认识

1989年第1期

内容加载中请稍等...