自动推理的应用谱系

自动推理程序在广泛应用中发挥重要作用的可能性，取决于其所提供的选项和参数，基于此制定所需的策略和方法论。本文聚焦于此类谱系，讨论了W. McCune的程序OTTER，涵盖在回答开放性问题方面的广泛成功，并触及一些关键作用的策略和方法论。应用包括：寻找第一个证明、发现单一公理、定位改进的公理系统以及简化现有证明。最后一种应用直接相关于R. Thiele发现的希尔伯特二十四问题——该问题通过合适的自动推理程序可被有效攻击，关乎证明的简化。方法论包括寻求更短证明、寻找避免不必要公理或术语类的证明、寻求更低等式或公式复杂度的证明，以及解决证明变量丰富性的问题。使用OTTER获得的证明类型为希尔伯特风格的公理化证明，包括可时常获得新见解的细节。我们包括仍然开放的问题和值得考虑的挑战。