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