模式匹配(例如在Prolog,ML系列语言和各种专家系统shell中找到)通常通过严格按顺序将元素的查询与数据匹配来进行操作.
然而,在诸如自动化定理证明之类的领域中,需要考虑到一些运算符是关联的和可交换的.假设我们有数据
A or B or C
和查询
C or $X
通过表面语法,这不匹配,但逻辑上它应该与$X绑定匹配,A or B因为or是关联和可交换的.
是否有任何语言的现有系统可以做这种事情？
我知道Iota减少用于减少/扩展递归函数.例如,给定以下简单递归函数的应用(自然数上的阶乘):
((fix fact (n:nat):nat := match n with | O => 1 | S m => n * fact m end) 2)
Iota缩减扩展了递归调用,有效地迭代递归函数一次:
Eval lazy iota in ((fix fact (n:nat):nat := match n with | O => 1 | S m => n * fact m end) 2).
= (fun n:nat =>
match n with
| 0 => 1
| S m =>
n *
(fix fact (m : nat) : nat :=
match m with
| 0 => …我一直在努力学习虽然原则上我喜欢异步防爆检查的主意,用伊莎贝尔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是逻辑编程的先驱.但我没有看到差异.但我想这不仅仅是语法.
我是二年级学生，我的离散数学 2 作业是制作一个自动定理证明器。我必须在 4 周内制作一个适用于命题逻辑的简单证明程序（假设证明始终存在）。到目前为止，我已经用谷歌搜索过，但 4 周后，那里的材料真的很难理解。谁能给我推荐一些适合初学者的书籍/网站/开源代码或一些有用的提示？先感谢您。
我正在尝试在OCaml中开发一个Coq策略,我已经构建了一个constr术语,现在想用这个术语在目标中实例化一个存在变量.我试图调用这个Evar_tactic.instantiate策略; 但它期望一个类型的论点 Tacinterp.interp_sign * Glob_term.glob_constr.无论如何转换constr到这种类型？或者我可以从OCaml级别实例化evars的任何其他方式？
其次,也有所谓的战术set,并pose在勒柯克.我找不到它们的定义.如果我想从OCaml中使用它们,我该怎么办？
我正在阅读伊德里斯教程。而且我无法理解下面的代码。
disjoint : (n : Nat) -> Z = S n -> Void
disjoint n p = replace {P = disjointTy} p ()
where
disjointTy : Nat -> Type
disjointTy Z = ()
disjointTy (S k) = Void
到目前为止，我发现......是
Void空类型，用于证明某些事情是不可能的。
替换：(x = y) -> P x -> P y 替换使用等式证明来转换谓词。
我的问题是：
哪一个是平等证明？(Z = S n)？
哪一个是谓词？功能disjointTy？
目的是什么disjointTy？disjointTy Z = () 是否意味着 Z 位于一个类型“land”() 中且 (S k) 位于另一块土地中Void？
Void 输出以什么方式表示矛盾？
诗。我所知道的证明是“凡事不匹配则为假”。或者“找到一件矛盾的事情”......
我想验证假设当然也是的Ring实例。在 Abelian Group 之前这很容易，但在实例中发生了一些奇怪的事情：Data.Complex.Complex ttRingRing
VerifiedRing t => VerifiedRing (Complex t) where
ringOpIsAssociative (l :+ li) (c :+ ci) (r :+ ri) =
?VerifiedRing_rhs_1
现在 Idris 自己进行了一些扩展，并且该洞得到以下类型：
(l <.> (c <.> r <+> inverse (ci <.> ri)) <+> inverse (li <.> (c <.> ri <+> ci <.> r))) :+ (l <.> (c <.> ri <+> ci <.> r) <+> li <.> (c <.> r <+> inverse (ci <.> ri))) =
((l <.> c <+> …我正在努力使Coq中的Free Selective Applicative Functors正式化，但是我在通过归纳法对具有非均匀类型参数的归纳数据类型进行挣扎。
让我简要介绍一下我正在处理的数据类型。在Haskell中，我们将自由选择函子编码为GADT：
data Select f a where
Pure :: a -> Select f a
Select :: Select f (Either a b) -> f (a -> b) -> Select f b
关键是b第二个数据构造函数中的存在类型变量。
我们可以将此定义转换为Coq：
Inductive Select (F : Type -> Type) (A : Set) : Set :=
Pure : A -> Select F A
| MkSelect : forall (B : Set), Select F (B + A) -> F (B -> A) -> Select F A. …有时我发现很难使用 Isabelle，因为我无法像在正常编程中那样使用“打印命令”。
例如，我想看看什么?thesis. 具体语义书说：
未知 ?thesis 隐含地与引理或 show 陈述的任何目标相匹配。下面是一个典型的例子：
我的愚蠢示例 FOL 证明是：
lemma
assumes "(? x. ? y. x ? y)"
shows "(?x. ? y. y ? x)"
proof (rule allI)
show ?thesis
但我收到错误：
proof (state)
goal (1 subgoal):
1. ?x. ?y. y ? x
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
?x. ?y. y ? x
但我知道为什么。
我期望
?thesis === ?x. ?y. …