文件名称：cooper:Idris 中的 Presburger 算术求解器
文件大小：7KB
文件格式：ZIP
更新时间：2024-07-05 16:30:52
Idris
库珀 使用 Cooper 方法实现 Presburger 算术求解器。 进步 步 实施的 证明 转换为否定范式 ✓ ✘ 删除冗余谓词 ✓ ✘ 将量化变量移动到文字的一侧 ✘ ✘ 从量化变量中删除系数 ✘ ✘ 构造左无限投影并去除量化 ✓ ✘ 为方便起见，每个步骤都有专门的 ADT。
【文件预览】：
cooper-master
----.gitignore(15B)
----README.md(615B)
----Step1()
--------Expr.idr(723B)
----Steps()
--------Factorize.idr(1KB)
--------EliminateQuantifier.idr(3KB)
--------NNF.idr(516B)
--------Dedup.idr(902B)
----Formulas()
--------Initial.idr(255B)
--------NotLess.idr(221B)
--------NNF.idr(217B)
----Internal()
--------Division.idr(2KB)
----Literals()
--------Reduced.idr(263B)
--------BaseLit.idr(227B)
--------Multiples.idr(358B)
--------Dedup.idr(223B)