希尔伯特系统 - 自动证明

我试图在Hilbert风格的系统中证明语句〜（a-> ~b）=> a。不幸的是，似乎不可能想出一个通用的算法来找到证据，但我正在寻找一种强力型策略。关于如何攻击这个的任何想法都是受欢迎的。     
2019-01-28 6 条评论
分享

没有找到相关结果

    已邀请:

    擅香

    Hilbert系统通常不用于自动定理证明。使用自然演绎编写计算机程序来进行校样要容易得多。从CS课程的材料：   关于希尔伯特系统的一些常见问题解答：   问：如何知道哪个公理   要使用的模式，以及哪些   替换做出？既然有   这是无限多种可能性   不可能全部尝试，即使在   princple。答：没有算法;在   最不简单的。相反，一个人   要聪明。在纯数学中，   这不是一个问题，因为   一个是最关心的   存在证明。但是，在   计算机科学应用，一个是   有兴趣自动扣除   过程，所以这是一个致命的缺陷。该   Hilbert系统通常不用于   自动定理证明。问：那么，为什么呢   人们关心希尔伯特吗？   系统？答：以modus ponens为主   单个演绎规则，它提供了一个   人类如何设计的可爱模型   数学证明。正如我们将看到，   更适合的方法   计算机实现产生证据   这不像人类那样。     
    2019-01-28 0 0
    分享

    揽芳僵迷仇

    在希尔伯特微积分中找到证据非常困难。 您可以尝试将后续微积分或自然演绎中的证明转换为希尔伯特微积分。     
    2019-01-28 0 0
    分享

    芯伶句餐绕

    您也可以通过设置¬α=α→approach来解决问题。然后我们可以采用Hilbert风格系统，如其中一个答案的附录所示，并通过添加以下两个公理和常量使其成为经典： Ex Falso Quodlibet：Eα：⊥→α 结节性Mirabilis：Mα：（¬α→α）→α ¬（α→¬β）→α的后续证明如下： α⊢α（身份） ⊥⊥β→⊥（Ex Falso Quodlibet） α→⊥，α⊢β→⊥（Impl简介左1＆amp; 2） α→⊥⊥α→（β→⊥）（Impl Intro Right 3） ⊥⊥α（Ex Falso Quodlibet） （α→（β→⊥））→⊥，α→⊥⊥α（Impl简介左4＆amp; 5） （α→（β→⊥））→⊥⊥α（Consequentia Mirabilis 6） ⊢（（α→（β→⊥））→⊥）→α（Impl Intro Right 7） 从这个后续证据中，可以提取lambda表达式。有可能 上述后续证明的lambda表达式如下： λy。（Mλz。（E（yλx。（E（z x））））） 该lambda表达式可以转换为SKI术语。有可能 上述lambda表达式的SKI术语如下： S（K M））（L2（L1（K（L2（L1（K I）））））） 其中L1 =（S（（S（K S））（（S（K K））I））） 和L2 =（S（K（S（K E）））） 这给出了以下Hilbert风格的证明： 引理1：链规则的弱化形式： 1：（（A→B）→（（C→A）→（C→B）））→（（（A→B）→（C→A））→（（A→B）→（C→B） ）））[链] 2：（（A→B）→（（C→（A→B））→（（C→A）→（C→B））））→（（（A→B）→（C→（A→A） B）））→（（A→B）→（（C→A）→（C→B））））[链] 3 :(（C→（A→B））→（（C→A）→（C→B）））→（（A→B）→（（C→（A→B））→（（C→ A）→（C→B））））[Verum Ex] 4：（C→（A→B））→（（C→A）→（C→B））[链] 5：（A→B）→（（C→（A→B））→（（C→A）→（C→B）））[MP 3,4] 6 :(（A→B）→（C→（A→B）））→（（A→B）→（（C→A）→（C→B）））[MP 2,5] 7：（（A→B）→（（A→B）→（C→（A→B））））→（（（A→B）→（A→B））→（（A→B）→ （C→（A→B））））[链] 8 :(（A→B）→（C→（A→B）））→（（A→B）→（（A→B）→（C→（A→B））））[Verum Ex] 9：（A→B）→（C→（A→B））[Verum Ex] 10：（A→B）→（（A→B）→（C→（A→B）））[MP 8,9] 11：（（A→B）→（A→B））→（（A→B）→（C→（A→B）））[MP 7,10] 12：（A→B）→（A→B）[身份] 13：（A→B）→（C→（A→B））[MP 11,12] 14：（A→B）→（（C→A）→（C→B））[MP 6,13] 15：（（A→B）→（C→A））→（（A→B）→（C→B））[MP 1,14] 引理2：Ex Falso的弱化形式： 1：（A→（（B→⊥）→（B→C）））→（（A→（B→⊥））→（A→（B→C）））[链] 2：（（B→⊥）→（B→C））→（A→（（B→⊥）→（B→C）））[Verum Ex] 3：（B→（⊥→C））→（（B→⊥）→（B→C））[链] 4：（⊥→C）→（B→（⊥→C））[Verum Ex] 5：⊥→C [Ex Falso] 6：B→（⊥→C）[MP 4,5] 7：（B→⊥）→（B→C）[MP 3,6] 8：A→（（B→⊥）→（B→C））[MP 2,7] 9：（A→（B→⊥））→（A→（B→C））[MP 1,8] 最终证明： 1 :(（（A→（B→⊥））→⊥）→（（（A→⊥）→A）→A））→（（（（A→（B→⊥））→⊥）→（（ A→⊥）→A））→（（（A→（B→⊥））→⊥）→A））[链] 2：（（（A→⊥）→A）→A）→（（（A→（B→⊥））→⊥）→（（（A→⊥）→A）→A））[Verum Ex] 3：（（A→⊥）→A）→A [Mirabilis] 4：（（A→（B→⊥））→⊥）→（（（A→⊥）→A）→A）[MP 2,3] 5 :(（（A→（B→⊥））→⊥）→（（A→⊥）→A））→（（（A→（B→⊥））→⊥）→A）[MP 1,4 ] 6 :(（（A→（B→⊥））→⊥）→（（A→⊥）→⊥））→（（（A→（B→⊥））→⊥）→（（A→⊥）→ A））[引理2] 7 :(（（A→（B→⊥））→⊥）→（（A→⊥）→（A→（B→⊥））））→（（（A→（B→⊥））→⊥） →（（A→⊥）→⊥））[引理1] 8 :(（A→⊥）→（A→（B→⊥）））→（（（A→（B→⊥））→⊥）→（（A→⊥）→（A→（B→⊥） ）））[Verum Ex] 9 :(（A→⊥）→（A→⊥））→（（A→⊥）→（A→（B→⊥）））[引理2] 10：（（A→⊥）→（A→A））→（（A→⊥）→（A→⊥））[引理1] 11：（A→A）→（（A→⊥）→（A→A））[Verum Ex] 12：A→A [身份] 13：（A→⊥）→（A→A）[MP 11,12] 14：（A→⊥）→（A→⊥）[MP 10,13] 15：（A→⊥）→（A→（B→⊥））[MP 9,14] 16 :(（A→（B→⊥））→⊥）→（（A→⊥）→（A→（B→⊥）））[MP 8,15] 17：（（A→（B→⊥））→⊥）→（（A→⊥）→⊥）[MP 7,16] 18：（（A→（B→⊥））→⊥）→（（A→⊥）→A）[MP 6,17] 19 :(（A→（B→⊥））→⊥）→A [MP 5,18] 相当长的证明！ 再见     
    2019-01-28 0 0
    分享

    盛虱

    哪个特定的希尔伯特系统？有吨。 可能最好的方法是在后续计算中找到证据并将其转换为希尔伯特系统。     
    2019-01-28 0 0
    分享

    肉脓措伪

    我用波兰表示法。 既然您引用了维基百科，我们假设我们的基础是 1 CpCqp。 2 CCpCqrCCpqCpr。 3 CCNpNqCqp。 我们要证明 NCaNb | - a。 我使用定理证明器Prover9。所以，我们需要将所有内容括起来。此外，Prover9的变量go（x，y，z，u，w，v5，v6，...，vn）。所有其他符号都被解释为函数或关系或谓词。所有公理在它们之前也需要一个谓词符号“P”，我们可以将其视为“可证明......”或更简单地“可证明”。 Prover9中的所有句子都需要一段时间才能结束。因此，公理1,2和3分别成为： 1 P（C（x，C（y，x）））。 2 P（C（C（x，C（y，z）），C（C（x，y），C（x，z））））。 3 P（C（C（N（x），N（y）），C（y，x）））。 我们可以将统一替代和脱离的规则结合到凝聚分离的规则中。在Prover9中，我们可以将其表示为： -P（C（x，y））| -P（x）| P（Y）。 “|”表示逻辑分离，“ - ”表示否定。 Prover9证明了矛盾。规则中的规则可以解释为“如果不是x，那么y是可证明的，或者不是x是可证明的，或者y是可证明的。”因此，如果它确实保持如果x，那么y是可证明的，则第一个析取失败。如果它确实证明x是可证明的，则第二个析取失败。因此，如果，如果x，那么y是可证明的，如果x是可证明的，那么第三个析取，即y可证明遵循规则。 现在我们不能在NCaNb中进行替换，因为它不是重言式。也不是“一个”。因此，如果我们放 P（N（C（A，N（B））））。 作为假设，Prover9会将“a”和“b”解释为nullary函数，从而有效地将它们转换为常量。我们也希望以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 ==========================
        
    2019-01-28 0 0
    分享
    为什么被折叠? 0 个回复被折叠

    要回复问题请先登录或注册

    或代码 OrCode.com 备案号：粤ICP备15020848号-1
    Escape time: 0.035896062850952