如果你喜欢“编程”的话 combinatory logic

• 您可以自动将一些逻辑问题“翻译”到另一个领域:证明组合逻辑项的相等性。
• 然后,你可以把答案翻译成希尔伯特式的原始逻辑问题的证明。

这种翻译的可能性由 Curry-Howard correspondence .

( ± β ) ±

但是,在否定不是问题的一部分的情况下,如果您已经在函数式编程或组合逻辑方面进行了实践,那么所提到的自动翻译(和反向翻译)可能会有所帮助。

---

当然,还有其他帮助,我们可以留在逻辑领域内:

• 在更直观的演绎系统中证明问题(例如。 natural deduction )
• 然后使用 metatheorem 它提供了“编译器”的可能性:将自然推理的“高级”证明翻译成希尔伯特式推理系统的“机器码”。我的意思是,例如,一个叫做 deduction theorem ".

---

至于定理证明者,据我所知,他们中的一些人的能力得到了扩展,以便他们能够利用交互式人工协助。例如。 Coq 就是这样。

---

---

附录

让我们看一个例子。如何证明 α ± ?

• 苦艾 _, 假设是一个公理方案,陈述了这句话 α ±
• 链规 _{± , ,} 假设是一个公理方案,陈述了这句话( ± ⊃ ) ( ) ± 预期是可推断的,为任何子内容实例化 ,
• 假肢 假设为推理规则:前提是 ± ⊃ β 是可以推断的,而且 ± ±

让我们证明一个定理: ± ± 对任何人来说都是可以推断的 提议

让我们介绍以下符号和缩写,发展“证明演算”:

• VEQ _{± ,} : ± ±
• _{± , ,} : ( ± ) ( ± ) ± ⊃
• 议员 :如果 ± β 和 ,然后也是

树形图表示法:

Axiom方案Verum ex quolibet:

[ VEQ _{± ,} ]
⊢ ± β ±

Axiom方案链规则:

铬 _{± , γ} ]
± ⊃ ⊃ γ ) ( ±

± ⊃ β ⊢ α
[ 议员 ]
β

证明树

让我们看一下证明的树形图表示:

铬 _{± ± ± ,} ] [ _{± , ⊃} ]
α ⊃( ) ± α ⊃ ± ⊃ ± ) ± ± ( ⊃ ) ±
议员 ][ VEQ _{, α} ]
± ± ± ± ± ± ± ±
[ ]
α ⊃ ±

证明公式

让我们看一个更简洁(代数?微积分?)的证明:

( 铬 _{± , ± ± ,} VEQ _{, ± ⊃ ±} ) VEQ _{, ±} ± ±

因此,我们可以用一个公式表示证明树:

• 树的分叉(modus ponens)通过简单的连接(括号)呈现,
• 树的叶子由相应的axiom名称的缩写表示。

证明演算 ,其中公理表示为 基组合子 ,并且波南斯方式被记为纯粹的 其“前提”子办公室:

例1

VEQ _, : ± ⊃ ⊃ ±

苦艾 ± 为陈述提供证据,即 ± ± 这是可以推断的。

VEQ _{± , ±} ± α ±

用 ± , ± ± ⊃ ±

VEQ _{± , ± ⊃ ±} : ( ± ± )

意思是

用 , ± ± 为陈述提供证据,即 ± ( ± ± ) 这是可以推断的。

例4

_, : ( ⊃ γ ) ( ± ) ± γ

意思是

链规 用 ± , ± ± β ) ± ⊃ γ

例5

铬 _{± ± ⊃ , ±} : [ ( ± ± ) ± ] ( ± ± ⊃ ± ) ± ±

意思是

链规 ± , ± α , ± ( ± ⊃ ± ) ± ] ( ⊃ ± ) ⊃ ± ± 这是可以推断的。

例6

_{, ± , α} VEQ _{, α} : ( ± ± ⊃ ± ) ±

如果我们联合起来 铬 _{± , α ,} 和 VEQ _{, ± ⊃ ±} 假肢 ,然后我们得到一个证明,证明以下陈述:( ± ⊃ ± ) ± ⊃ ± 这是可以推断的。

例7

铬 _{± , ± , ±} VEQ _{± ± α} ) VEQ _{± , ±} : ±

如果我们结合计算机证明( _{, ± ± , ±} )连同 VEQ _{± ± ±} (via 假肢 ),然后我们得到一个更复杂的证明。这证明了以下说法: ± ⊃ ± 这是可以推断的。

组合逻辑

虽然以上这些确实为期望定理提供了一个证明,但它似乎很不直观。看不出人们是如何“找到”证据的。

非类型组合逻辑

Combinatory logic 也可以看作是一种极简的函数式编程语言。尽管其极简主义,它完全图灵完成,但更重要的是,人们可以编写相当直观和复杂的程序,即使在这种看似模糊的语言中,以模块化和可重用的方式,通过从“正常”函数编程和一些代数见解中获得的一些实践。

添加键入规则

组合逻辑也有类型化的变体。语法中增加了类型,甚至除了减少规则之外,还增加了类型规则。

• K _{, β} 被选为基本组合符, inhabiting type ± ±
• _{± ,} 被选为基本组合符,居住类型( ± ) ( ± ) ± .

申请的打字规则:

• 如果 X 居住类型 → β 和 Y ± 然后 X Y 居住类型 .

符号和缩写

• K _{± β} : ±
• s _{α , β ,} : ( ± β → ) ( ± β )* → ± → γ .
• 如果 : ± β 和 : ± 然后 X : β .

咖喱霍华德信件

可以看出,在证明演算和这种类型的组合逻辑中,“模式”是同构的。

• 苦艾 证明演算的公理对应于 组合逻辑的基组合子
• 这个 证明演算的公理对应于 s 组合逻辑的基组合子
• 这个 假肢 证明演算中的推理规则对应于组合逻辑中的“应用”运算。
• 逻辑的“条件”连接符对应于类型理论(和类型组合逻辑)的类型构造函数

但好处是什么?为什么我们要把问题转化为组合逻辑?一、 就我个人而言,我觉得它有时很有用,因为函数式编程是一个有大量文献的东西,并且应用于实际问题中。当人们被迫在每天的编程任务和实践中使用它时,他们可以习惯它。函数编程实践中的一些技巧和提示可以很好地用于组合逻辑约简。如果一个“转移”的实践在组合逻辑中发展,那么它也可以在Hilbert系统中找到证明。

外部链接

• 韦德勒,菲利普(1989)。 Theorems for free!

链接(或书籍)如何学习直接在组合逻辑中编程的方法和实践:

• 大卫·马多尔(2003年)。 The Unlambda Programming Language. Unlambda: Your Functional Programming Language Nightmares Come True .
• 咖喱、哈斯凯尔酒店;费斯,罗伯特,;威廉·克雷格(1958年)。 . . 阿姆斯特丹:北荷兰出版公司。
• 约翰·特罗普(1999年)。 二元Lambda演算与组合逻辑 . 可从作者的网站下载PDF和Postscript格式 John's Lambda Calculus and Combinatory Logic Playground .

material of a CS course :

关于希尔伯特系统的一些常见问题: 要使用的模式,以及 要进行替换吗?既然有 不可能全部尝试,即使是在 普林斯波。答:没有算法;在 要聪明。在纯数学中, 这不被视为问题,因为 一个是最关心的问题 计算机科学应用,一个是 有兴趣自动扣除吗 这是一个致命的缺陷。这个 Hilbert系统通常不用于 自动定理证明。问:那么,为什么 人们关心希尔伯特吗 单一演绎规则,它提供了 更容易接受的方法 计算机实现生成证明 它们不像人类。

在希尔伯特微积分中寻找证明是非常困难的。

1. 哪个特定的希尔伯特系统?有很多。
2. 也许最好的方法是在后续微积分中找到证明,并将其转换为希尔伯特系统。

我用 Polish notation .

既然你引用了维基百科,我们假设我们的基础是

1 CpCqp。

2 CCPCRCCPQCPR。

3 CCNpNqCqp。

我们想证明

NCaNb |-a。

我使用定理证明器 Prover9 . 所以,我们需要把所有内容都括起来。此外,Prover9的变量为go(x、y、z、u、w、v5、v6、…、vn)。所有其他符号都被解释为函数、关系或谓词。所有的公理在它们之前都需要一个谓词符号“P”,我们可以认为它的意思是“它是可证明的……”或者更简单地说是“可证明的”。Prover9中的所有句子都需要以句号结尾。因此,公理1、公理2和公理3分别成为:

1p(C(x,C(y,x)))。

2p(C(C(x,C(y,z)),C(C(x,y),C(x,z)))。

3p(C(C(N(x),N(y)),C(y,x)))。

我们可以把统一替换和分离的规则结合到统一规则中 condensed detachment . 在Prover9中,我们可以表示为:

-P(C(x,y))|-P(x)| P(y)。

“|”表示逻辑析取,“-”表示否定。证明人用矛盾来证明。这条用文字表述的规则可以解释为“如果x是可证明的,那么y是可证明的,或者x不是可证明的,或者y是可证明的。”因此,如果它认为如果x是可证明的,那么y是可证明的,那么第一个析取就失败了。如果它认为x是可证明的,那么第二个析取失败。所以,如果,如果x,那么y是可证明的,如果x是可证明的,那么第三个间断,即y是可证明的,遵循规则。

P(N(C(a,N(b)))。

假设Prover9将“a”和“b”解释为 函数,从而有效地将它们转换为常量。我们也希望把P(a)作为我们的目标。

现在,我们还可以使用各种定理证明策略“调优”Prover9,如加权、共振、子公式、选择给定比率、电平饱和(甚至发明我们自己的)。我将稍微使用提示策略,将所有假设(包括推理规则)和目标转换为提示。我还将把最大权重降低到40,并将最大变量数设为5。

set(ignore_option_dependencies). % GUI handles dependencies

if(Prover9). % Options for Prover9
assign(max_seconds, -1).
assign(max_weight, 40).
end_if.

if(Mace4).   % Options for Mace4
assign(max_seconds, 60).
end_if.

if(Prover9). % Additional input for Prover9
formulas(hints).
-P(C(x,y))|-P(x)|P(y).
P(C(x,C(y,x))).
P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).
P(C(C(N(x),N(y)),C(y,x))).
P(N(C(a,N(b)))).
P(a).
end_of_list.
assign(max_vars,5).
end_if.

formulas(assumptions).

-P(C(x,y))|-P(x)|P(y).
P(C(x,C(y,x))).
P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).
P(C(C(N(x),N(y)),C(y,x))).
P(N(C(a,N(b)))).

end_of_list.

formulas(goals).

P(a).

end_of_list.

这是它给我的证据:

============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 1312 was started by Doug on Machina2,
Mon Jun  9 22:35:37 2014
The command was "/cygdrive/c/Program Files (x86)/Prover9-Mace43/bin-win32/prover9".
============================== end of head ===========================

============================== end of input ==========================

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.01) seconds.
% Length of proof is 23.
% Level of proof is 9.
% Maximum clause weight is 20.
% Given clauses 49.

1 P(a) # label(non_clause) # label(goal).  [goal].
2 -P(C(x,y)) | -P(x) | P(y).  [assumption].
3 P(C(x,C(y,x))).  [assumption].
4 P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).  [assumption].
5 P(C(C(N(x),N(y)),C(y,x))).  [assumption].
6 P(N(C(a,N(b)))).  [assumption].
7 -P(a).  [deny(1)].
8 P(C(x,C(y,C(z,y)))).  [hyper(2,a,3,a,b,3,a)].
9 P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))).  [hyper(2,a,4,a,b,4,a)].
12 P(C(C(C(N(x),N(y)),y),C(C(N(x),N(y)),x))).  [hyper(2,a,4,a,b,5,a)].
13 P(C(x,C(C(N(y),N(z)),C(z,y)))).  [hyper(2,a,3,a,b,5,a)].
14 P(C(x,N(C(a,N(b))))).  [hyper(2,a,3,a,b,6,a)].
23 P(C(C(a,N(b)),x)).  [hyper(2,a,5,a,b,14,a)].
28 P(C(C(x,C(C(y,x),z)),C(x,z))).  [hyper(2,a,9,a,b,8,a)].
30 P(C(x,C(C(a,N(b)),y))).  [hyper(2,a,3,a,b,23,a)].
33 P(C(C(x,C(a,N(b))),C(x,y))).  [hyper(2,a,4,a,b,30,a)].
103 P(C(N(b),x)).  [hyper(2,a,33,a,b,3,a)].
107 P(C(x,b)).  [hyper(2,a,5,a,b,103,a)].
113 P(C(C(N(x),N(b)),x)).  [hyper(2,a,12,a,b,107,a)].
205 P(C(N(x),C(x,y))).  [hyper(2,a,28,a,b,13,a)].
209 P(C(N(a),x)).  [hyper(2,a,33,a,b,205,a)].
213 P(a).  [hyper(2,a,113,a,b,209,a)].
214 $F.  [resolve(213,a,7,a)].

============================== end of proof ==========================