我试图从"精益证明中的证据"第7章中理解归纳类型.
我为自己设定了一个任务,证明自然数的继承者有平等的替代属性:
inductive natural : Type
| zero : natural
| succ : natural -> natural
lemma succ_over_equality (a b : natural) (H : a = b) :
(natural.succ a) = (natural.succ b) := sorry
经过一些猜测和相当详尽的搜索后,我能够满足编译器的几种可能性:
lemma succ_over_equality (a b : natural) (H : a = b) :
(natural.succ a) = (natural.succ b) :=
eq.rec_on H (eq.refl (natural.succ a))
--eq.rec_on H rfl
--eq.subst H rfl
--eq.subst H (eq.refl (natural.succ a))
--congr_arg (? (n : natural), (natural.succ n)) H …定理证明工具z3花了很多时间来解决一个公式,我相信它应该能够轻松处理.为了更好地理解这一点并可能优化我对z3的输入,我想看到z3生成的内部约束作为其求解过程的一部分.当从命令行使用z3时,如何打印z3为其后端解算器生成的公式？
当我在伊莎贝尔中说出一个引理时,我经常打字nitpick,如果这不能给我一个反例.然后我键入sledgehammer以尝试自动查找证明.
我想知道:是否可以调用Nitpick和Sledgehammer以便它们同时运行？由于Sledgehammer已经将我的引理发送给了许多自动证明器,这些证明器中的其中一个实际上不是像Nitpick那样的反例调查器吗？
我想将以下Haskell代码转换为Agda:
import Control.Arrow (first)
import Control.Monad (join)
safeTail :: [a] -> [a]
safeTail [] = []
safeTail (_:xs) = xs
floyd :: [a] -> [a] -> ([a], [a])
floyd xs [] = ([], xs)
floyd (x:xs) (_:ys) = first (x:) $ floyd xs (safeTail ys)
split :: [a] -> ([a], [a])
split = join floyd
这使我们能够有效地将列表拆分为两个:
split [1,2,3,4,5] = ([1,2,3], [4,5])
split [1,2,3,4,5,6] = ([1,2,3], [4,5,6])
所以,我试图将此代码转换为Agda:
floyd : {A : Set} ? List A ? List A ? List …haskell functional-programming theorem-proving agda floyd-cycle-finding
我正在阅读Terry Tao的真实分析教科书,它从自然数字中建立起基础数学.通过尽可能多地形式化证明,我希望能够熟悉Idris和依赖类型.
我已经定义了以下数据类型:
data GE: Nat -> Nat -> Type where
Ge : (n: Nat) -> (m: Nat) -> GE n (n + m)
表示一个自然数大于或等于另一个自然数的命题.
我目前正在努力证明这种关系的反身性,即用签名来构建证明
geRefl : GE n n
我的第一次尝试就是尝试geRefl {n} = Ge n Z,但这种类型Ge n (add n Z).为了使这与所需的签名统一起来,我们显然必须进行某种重写,可能涉及引理
plusZeroRightNeutral : (left : Nat) -> left + fromInteger 0 = left
我最好的尝试如下:
geRefl : GE n n
geRefl {n} = x
where x : GE n (n + Z)
x = rewrite plusZeroRightNeutral n …Monadic一阶逻辑，其中所有谓词都恰好采用一个参数，是一阶逻辑的已知可判定片段。测试公式是否可以满足此逻辑是可以确定的，并且存在基于分辨率的方法来确定这一点。
我处于需要测试一些单子一阶逻辑语句的可满足性的情况。我意识到我将达到理论上的复杂性极限，但我希望在常见情况下能够获得合理的性能。
现在，存在大量的定理证明，它们提供了解决一阶逻辑问题的快速方法。其中包括Vampire，SPASS，E，以及Z3和CVC4的量词扩展。但是，由于不确定性，不能保证它们停止运行。
我的问题
在现有的定理证明者中，有谁能保证在给定单子式公式作为输入时停止？还是有一种方法可以使用它们（以某种方式）有效地测试单子公式的可满足性？
formal-verification proof theorem-proving first-order-logic smt
在精益中，我有时想将一种rw策略应用于多个相同术语中的一个。例如我有一个目标
\xe2\x8a\xa2 0 = 0\n我想要rw它
\xe2\x8a\xa2 a * 0 = 0\n我也有
\nmul_zero (a : mynat) :\n a * 0 = 0\n现在我应该能够重写0to a * 0。然而尝试
rw \xe2\x86\x90 zero_mul a,\n给我
\n\xe2\x8a\xa2 a * 0 = a * 0\n这不是我想要的！
\n精益这样做有什么原因吗？是否有某种方法可以将重写仅应用于一个术语？
\n我在Coq玩,试图创建一个排序列表.我只是想要一个带有列表的函数,[1,2,3,2,4]并返回类似的东西Sorted [1,2,3,4]- 即取出坏的部分,但实际上并没有对整个列表进行排序.
我想我会先定义一个lesseq类型的函数(m n : nat) -> option (m <= n),然后我可以非常轻松地模拟匹配.也许这是一个坏主意.
我现在遇到的问题的症结在于(片段,底部的整个功能)
Fixpoint lesseq (m n : nat) : option (m <= n) :=
match m with
| 0 => match n with
| 0 => Some (le_n 0)
...
不是类型的; 它说它期待一个option (m <= n),但它Some (le_n 0)有类型option (0 <= 0).我不明白,因为很明显,两者m并n在这方面零,但我不知道如何告诉勒柯克说.
整个功能是:
Fixpoint lesseq (m n : nat) : option (m <= …我一直在努力学习虽然原则上我喜欢异步防爆检查的主意,用伊莎贝尔2016年,我不喜欢伊莎贝尔/ jEdit的为许多原因,其中最严重的是,它使用了太多的内存(为了我).
如果我可以使用Isabelle 2016中的旧版Proof General,那就太棒了.我将变量设置isa-isabelle-command为指向bin/isabelleIsabelle分发目录下的文件.当我使用Proof General的菜单启动Isabelle时,Emacs挂起,当我打断它时C-g,我在*isabelle*缓冲区中得到以下内容.
> val it = (): unit
^BException- ERROR "Bad socket name: \"I\"" raised
我知道这个站点上的旧帖子表明,Proof General用来与定理证明者通信的Isabelle组件被删除了.这是(仍然)Isabelle 2016的真实情况吗？如何在较新版本的Isabelle中使用Proof General？
逻辑编程和自动定理证明(ATP)之间有什么区别(例如使用E-Prover,Spass或Princess)？
我搜索了很多,我发现的唯一信息是ATP是逻辑编程的先驱.但我没有看到差异.但我想这不仅仅是语法.