GAPT：证明理论的通用架构 GAPT是主要在维也纳科技大学开发的证明理论框架。 GAPT包含证明理论和自动推论中常见的数据结构，算法，解析器和其他组件。 与自动交互定理证明者（其重点是证明的构造）相反，GAPT专注于证明的转换和进一步处理。 网站： ： 联系人： 例 GAPT支持的众多功能之一是的实现。 您可以通过以下方式在GAPT中自动生成Herbrand析取： Escargot .getExpansionProof( fof " P(c) ∨ P(d) → ∃x P(x) " ).map(_.deep) 它返回以下Herbrand析取关系（右侧的量词已扩展）： Some(