fyp:我在斯特拉斯克莱德大学的最后一年的项目 源码

阿格达提供证据的问题解决者 报告,包括为其编写的所有软件,在report目录中。 可以通过运行make将其编译为PDF。 请注意,要使此方法成功,需要编译所有有文化的Agda文件。 这些是为Agda 2.5.3编写的,并且取决于标准库。 要仅编译报告所依赖的Agda模块,请运行make modules 。 报告使用TeX包catchfilebetweentags来包含部分识字的Agda模块,其中包含以下内容: Monoids :关于Monoid方程的完整求解器。 CommutativeRings :来自Agda标准库的可交换环上方程的求解器。 Normalisation :Presburger公式的未经验证的归一化。 Presburger :用于Presburger算术的Omega测试,已验证但未完成。 Adaptation :围绕Presburger和Normalisatio