Targeted Proof Machines in Combinatorics

Zeilberger计划在组合学和相关领域开发自动发现和证明结果的算法。特别是，他计划机械化Dodgson的方法来评估超几何行列式，使用计算语言学的技术来经验地发现并严格证明组合族的“语法”，并开发一个多变量理性生成函数的计算Ansatz。他还建议研究计算化学技术的组合类似物，并试图证明海曼的对角谐波猜想。这项研究属于组合学的一般领域。组合学的目标之一是找到研究离散对象集合如何排列的有效方法。离散系统的行为对现代通信极为重要。例如，大型网络的设计，比如那些出现在电话系统中的网络，以及计算机科学中处理离散对象集的算法设计，这就利用了组合研究。这项研究也属于符号计算的一般领域，它试图教会计算机执行以前需要大量人力资源的研究。这一领域的进展有望对科学技术产生重要影响。

Zeilberger 9732602 Zeilberger plans to develop algorithms for automatic discovery and proof of results in combinatorics and related areas. In particular, he plans to mechanize Dodgson's method evaluating hypergeometric determinants, to use techniques from computational linguistics to empirically discover and then rigorously prove `grammars' of combinatorial families, and to develop a computational Ansatz for multi-variate rational generating functions. He also proposes to investigate combinatorial analogs of techniques from computational chemistry and to try to prove Haiman's Diagonal Harmonics conjecure. This research is in the general area of Combinatorics. One of the goals of Combinatorics is to find efficient methods of studying how discrete collections of objects can be arranged. The behavior of discrete systems is extremely important to modern communications. For example, the design of large networks, such as those occurring in telephone systems, and the design of algorithms in computer science deal with discrete sets of objects, and this makes use of combinatorial research. This research is also in the general area of Symbolic Computation, that attempts to teach computers to perform research that previously required extensive human resources. Progress in this area promises to have important ramifications to science and technology.