文件名称：apia:Haskell程序，用于使用一阶逻辑的自动定理证明器来证明用Agda编写的一阶定理
文件大小：329KB
文件格式：ZIP
更新时间：2024-05-29 23:27:28
Haskell
阿皮亚 描述 Apia是Haskell程序，用于使用一阶逻辑（ATP）的自动定理证明器来证明用编写的一阶定理。 在调用ATP之前，将Agda公式转换为语言。 Apia通过结合交互式和自动证明来对功能程序进行推理（请参阅 ）。 先决条件 格拉斯哥Haskell编译器（ ） Apia支持Agda上游支持的GHC版本，即7.10.3、8.0.2、8.2.2和8.4.3。 使用以下方法检查您的版本： $ ghc --version Agda的扩展版本 我们已经扩展了Agda的开发版本，以便处理新的内置ATP-pragma。 Apia程序需要此Agda的扩展版本。 ATP：Apia可以使用离线或在线ATP 离线ATP 当前支持的脱机ATP是： 三磷酸腺苷 测试版 CVC4 1.6 E 2.1马哈拉尼山 春分5.0alpha（2010-06-29） ileanCoP 1.3b