如何解决重用策略证明可判定性
我对Presburger算术有一个抽象的语法,还有一个确定给定公式的命题表示法的定点函数(您可以在这里找到https://gist.github.com/d4hines/d9a0c674f324cab46d2cf0967bde1ac3)。
我想证明任何给定公式的真值都是可确定的。由于它是Presburger算术,因此我知道它必须是可判定的。我听说Presburger算术的决策程序非常复杂。我想重用existing one in Coq。
我该怎么做?
谢谢!
解决方法
lia
对您没有太大帮助的原因有很多。
-
lia并没有解决像
exists x : Z,2 < x < 4
这样的小的真实目标:对于Prestburger算术而言,这种策略并不完整 -
即使
lia
对于Presburger来说是完整的,它也可以作为一个预言:每次需要一个真公式时,便会给您一个答案。但是当出现错误公式时,lia
只会对Coq说我做不到,并没有说我有一个证明不能做到这一点。换句话说,证明程序完成的信息可能不会作为 Coq可读证明存储在Coq系统中。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。