gapt:GAPT:证明理论的通用架构 源码

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