| 【educoder】离散数学：自然推理系统 | 您所在的位置：网站首页 › 离散数学推理规则步骤 › 【educoder】离散数学：自然推理系统 |
【educoder】离散数学：自然推理系统
|
【educoder】离散数学：自然推理系统
相关知识
1. 目前支持以下这些规则的检查：
基于教材使用的符号进行了转换，请注意以下与教材符号的对应说明： 对带量词的公式，需要特别小心： 所有的符号都是英文半角符号，不支持中文全角符号，如。、，；等 书写证明时的要求： 第一行： Premise: ，各前件之间用“,”隔开，如： Premise: ((Exist x)P(x)) -> (All x)((P(x)/Q(x)) -> R(x)), (Exist x)P(x), (Exist x)Q(x) 第二行： Conclusion：，一般只有一个，如： Conclusion: (Exist x)(Exist y)(R(x)/\R(y)) 答题模版中通常会预先给出第一、二行，无需自己输入。 此后可空几行或不空行开始编写证明步骤； 格式： ae或ei规则示例： 下图的第6、10、11步 下图是用于编写证明时，25条规则的简称： 下面是一个示例： Premise: ~B, A->B Conclusion: ~A ~B, A->B, A |- A prem ~B, A->B, A |- A->B prem ~B, A->B, A |- B imple 1,2 ~B, A->B, A |- ~B prem ~B, A->B |- ~A ni 3,4 编程要求请按说明，严格按格式撰写证明过程。 测试说明平台会对你编写的证明进行检查，出现“证明过程正确”表明编写的证明是正确的。 如出现其他问题，请先检查是否按规定的格式编写证明。 第1关：6.1节第1题a) 任务描述不用导出规则，请证明：⊢(A→(B→C))↔(B→(A→C))。 Premise: Conclusion: (A->(B->C))(B->(A->C)) 1. A->(B->C),B,A |- A prem 2. A->(B->C),B,A |- A->(B->C) prem 3. A->(B->C),B,A |- B->C imple 1,2 4. A->(B->C),B,A |- B prem 5. A->(B->C),B,A |- C imple 4,3 6. A->(B->C),B |- A->C impli 5 7. A->(B->C) |- B->(A->C) impli 6 8. B->(A->C),A,B |- B prem 9. B->(A->C),A,B |- B->(A->C) prem 10. B->(A->C),A,B |- A->C imple 8,9 11. B->(A->C),A,B |- A prem 12. B->(A->C),A,B |- C imple 11,10 13. B->(A->C),A |- B->C impli 12 14. B->(A->C) |- A->(B->C) impli 13 15. |- (A->(B->C))(B->(A->C)) equivi 7,14 第2关：6.1节第1题b)-1 任务描述不用导出规则，请证明：(A∨B)∨C⊢A∨(B∨C)。 Premise: (A\/B)\/C Conclusion: A\/(B\/C) 1. A |- A prem 2. A |- A\/(B\/C) ori 1 3. B |- B prem 4. B |- B\/C ori 3 5. B |- A\/(B\/C) ori 4 6. C |- C prem 7. C |- B\/C ori 6 8. C |- A\/(B\/C) ori 7 9. A\/B |- A\/(B\/C) ore 2,5 10. (A\/B)\/C |- A\/(B\/C) ore 8,9 第3关：6.1节第1题b)-2 任务描述不用导出规则，请证明：A∨(B∨C)⊢(A∨B)∨C。 Premise: A\/(B\/C) Conclusion: (A\/B)\/C 1. C |- C prem 2. C |- (A\/B)\/C ori 1 3. B |- B prem 4. B |- A\/B ori 3 5. B |- (A\/B)\/C ori 4 6. A |- A prem 7. A |- A\/B ori 6 8. A |- (A\/B)\/C ori 7 9. B\/C |- (A\/B)\/C ore 2,5 10. A\/(B\/C) |- (A\/B)\/C ore 8,9 第4关：6.1节第1题c) 任务描述不用导出规则，请证明：⊢(A→B)↔(¬B→¬A)。 Premise: Conclusion: (A->B)(~B -> ~A) 1. A->B,~B,A |- A->B prem 2. A->B,~B,A |- A prem 3. A->B,~B,A |- B imple 1,2 4. A->B,~B,A |- ~B prem 5. A->B,~B |- ~A ni 3,4 6. A->B |- ~B->~A impli 5 7. ~B->~A,A,~B |- ~B->~A prem 8. ~B->~A,A,~B |- ~B prem 9. ~B->~A,A,~B |- ~A imple 7,8 10. ~B->~A,A,~B |- A prem 11. ~B->~A,A |- ~~B ni 9,10 12. ~B->~A,A |- B nne 11 13. ~B->~A |- A->B impli 12 14. |- (A->B)(~B->~A) equivi 6,13 第5关：6.1节第1题d)-1 任务描述不用导出规则，请证明：A∧¬A⊢F。 Premise: A/\~A Conclusion: F 1. A/\~A |- A/\~A prem 2. A/\~A |- A ande 1 3. A/\~A |- ~A ande 1 4. A/\~A |- F ne 2,3 第6关：6.1节第1题d)-2 任务描述不用导出规则，请证明：F⊢A∧¬A。 Premise: F Conclusion: A/\~A 1. F |- ~F fi 2. F |- F prem 3. F |- A/\~A ne 1,2 第7关：6.1节第1题e)-1 任务描述不用导出规则，请证明：A→(B→C)⊢A∧B→C。 Premise: A->(B->C) Conclusion: A/\B->C 1. A->(B->C),A/\B |- A/\B prem 2. A->(B->C),A/\B |- A ande 1 3. A->(B->C),A/\B |- B ande 1 4. A->(B->C),A/\B |- A->(B->C) prem 5. A->(B->C),A/\B |- B->C imple 2,4 6. A->(B->C),A/\B |- C imple 3,5 7. A->(B->C) |- A/\B->C impli 6 第8关：6.1节第1题e)-2 任务描述不用导出规则，请证明：A∧B→C⊢A→(B→C)。 Premise: A/\B->C Conclusion: A->(B->C) 1. A/\B->C,A,B |- A prem 2. A/\B->C,A,B |- B prem 3. A/\B->C,A,B |- A/\B andi 1,2 4. A/\B->C,A,B |- A/\B->C prem 5. A/\B->C,A,B |- C imple 3,4 6. A/\B->C,A |- B->C impli 5 7. A/\B->C |- A->(B->C) impli 6 第9关：6.1节第2题a) 任务描述不用导出规则，请证明：(∀x)P(x)⊢(∃x)P(x)。 Premise:(All x)P(x) Conclusion:(Exist x)P(x) Premise:(All x)P(x) Conclusion:(Exist x)P(x) 1. (All x)P(x) |- (All x)P(x) prem 2. (All x)P(x) |- P(t) ae 1 (t/x) 3. (All x)P(x) |- (Exist x)P(x) ei 2 (t/x) 第10关：6.1节第2题b) 任务描述不用导出规则，请证明：(∃x)(∀y)P(x,y)⊢(∀y)(∃x)P(x,y)。 Premise: (Exist x)(All y)P(x,y) Conclusion: (All y)(Exist x)P(x,y) 1. P(x,y) |- P(x,y) prem 2. (All y)P(x,y) |- P(x,y) lai 1 3. (Exist x)(All y)P(x,y) |- (Exist x)P(x,y) eei 2 4. (Exist x)(All y)P(x,y) |- (All y)(Exist x)P(x,y) ai 3 第11关：6.1节第2题c) 任务描述不用导出规则，请证明：(∀y)P(x)∨(∀x)Q(x)⊢(∀x)(P(x)∨Q(x))。 Premise: (All x)P(x)\/(All x)Q(x) Conclusion: (All x)(P(x)\/Q(x)) 1. P(x) |- P(x) prem 2. P(x) |- P(x)\/Q(x) ori 1 3. (All x)P(x) |- (All x)(P(x)\/Q(x)) aai 2 4. Q(x) |- Q(x) prem 5. Q(x) |- P(x)\/Q(x) ori 4 6. (All x)Q(x) |- (All x)(P(x)\/Q(x)) aai 5 7. (All x)P(x)\/(All x)Q(x) |- (All x)(P(x)\/Q(x)) ore 3,6 第12关：6.1节第2题d)-1 任务描述不用导出规则，请证明：(∀x)(A→P(x))⊢A→(∀y)P(x)，其中x不是A中的自由变元。 Premise: (All x)(A->P(x)) Conclusion: A->(All x)P(x) 1. A->P(x) |- A->P(x) prem 2. (All x)(A->P(x)) |- A->P(x) lai 1 3. (All x)(A->P(x)),A |- A prem 4. (All x)(A->P(x)),A |- A->P(x) premi 2 5. (All x)(A->P(x)),A |- P(x) imple 4,3 6. (All x)(A->P(x)),A |- (All x)P(x) ai 5 7. (All x)(A->P(x)) |- A->(All x)P(x) impli 6 第13关：6.1节第2题d)-2 任务描述不用导出规则，请证明：A→(∀y)P(x)⊢(∀x)(A→P(x))，其中x不是A中的自由变元。 Premise: A->(All x)P(x) Conclusion: (All x)(A->P(x)) 1. A->(All x)P(x),A |- A prem 2. A->(All x)P(x),A |- A->(All x)P(x) prem 3. A->(All x)P(x),A |- (All x)P(x) imple 1,2 4. A->(All x)P(x),A |- P(x) ae 3 (x/x) 5. A->(All x)P(x) |- A->P(x) impli 4 6. A->(All x)P(x) |- (All x)(A->P(x)) ai 5 第14关：6.1节第2题e)-1 任务描述不用导出规则，请证明：(∃x)(P(x)∨Q(x))⊢(∃x)P(x)∨(∃x)Q(x)。 Premise: (Exist x)(P(x)\/Q(x)) Conclusion: (Exist x)P(x)\/(Exist x)Q(x) 1. P(x) |- P(x) prem 2. P(x) |- (Exist x)P(x) ei 1 (x/x) 3. P(x) |- (Exist x)P(x)\/(Exist x)Q(x) ori 2 4. Q(x) |- Q(x) prem 5. Q(x) |- (Exist x)Q(x) ei 4 (x/x) 6. Q(x) |- (Exist x)P(x)\/(Exist x)Q(x) ori 5 7. P(x)\/Q(x) |- (Exist x)P(x)\/(Exist x)Q(x) ore 6,3 8. (Exist x)(P(x)\/Q(x)) |- (Exist x)P(x)\/(Exist x)Q(x) lei 7 第15关：6.1节第2题e)-2 任务描述不用导出规则，请证明：(∃x)P(x)∨(∃x)Q(x)⊢(∃x)(P(x)∨Q(x))。 Premise: (Exist x)P(x)\/(Exist x)Q(x) Conclusion: (Exist x)(P(x)\/Q(x)) 1. P(x) |- P(x) prem 2. P(x) |- P(x)\/Q(x) ori 1 3. (Exist x)P(x) |- (Exist x)(P(x)\/Q(x)) eei 2 4. Q(x) |- Q(x) prem 5. Q(x) |- P(x)\/Q(x) ori 4 6. (Exist x)Q(x) |- (Exist x)(P(x)\/Q(x)) eei 5 7. (Exist x)P(x)\/(Exist x)Q(x) |- (Exist x)(P(x)\/Q(x)) ore 3,6 第16关：6.1节第2题f)-1 任务描述不用导出规则，请证明：(∀x)(P(x)∧Q(x))⊢(∀x)P(x)∧(∀x)Q(x)。 Premise: (All x)(P(x)/\Q(x)) Conclusion: (All x)P(x)/\(All x)Q(x) 1. P(x)/\Q(x) |- P(x)/\Q(x) prem 2. P(x)/\Q(x) |- P(x) ande 1 3. P(x)/\Q(x) |- Q(x) ande 1 4. (All x)(P(x)/\Q(x)) |- (All x)P(x) aai 2 5. (All x)(P(x)/\Q(x)) |- (All x)Q(x) aai 3 6. (All x)(P(x)/\Q(x)) |- (All x)P(x)/\(All x)Q(x) andi 4,5 第17关：6.1节第2题f)-2 任务描述不用导出规则，请证明：(∀x)P(x)∧(∀x)Q(x)⊢(∀x)(P(x)∧Q(x)) Premise: (All x)P(x)/\(All x)Q(x) Conclusion: (All x)(P(x)/\Q(x)) 1. (All x)P(x)/\(All x)Q(x) |- (All x)P(x)/\(All x)Q(x) prem 2. (All x)P(x)/\(All x)Q(x) |- (All x)P(x) ande 1 3. (All x)P(x)/\(All x)Q(x) |- P(x) ae 2 (x/x) 4. (All x)P(x)/\(All x)Q(x) |- (All x)Q(x) ande 1 5. (All x)P(x)/\(All x)Q(x) |- Q(x) ae 4 (x/x) 6. (All x)P(x)/\(All x)Q(x) |- P(x)/\Q(x) andi 3,5 7. (All x)P(x)/\(All x)Q(x) |- (All x)(P(x)/\Q(x)) ai 6 第18关：6.1节第2题g) 任务描述不用导出规则，请证明：(∃x)P(x)→(∀x)Q(x)⊢(∀x)(P(x)→Q(x))。 Premise: (Exist x)P(x)->(All x)Q(x) Conclusion: (All x)(P(x)->Q(x)) 1. (Exist x)P(x)->(All x)Q(x),P(x) |- P(x) prem 2. (Exist x)P(x)->(All x)Q(x),P(x) |- (Exist x)P(x) ei 1 (x/x) 3. (Exist x)P(x)->(All x)Q(x),P(x) |- (Exist x)P(x)->(All x)Q(x) prem 4. (Exist x)P(x)->(All x)Q(x),P(x) |- (All x)Q(x) imple 2,3 5. (Exist x)P(x)->(All x)Q(x),P(x) |- Q(x) ae 4 (x/x) 6. (Exist x)P(x)->(All x)Q(x) |- P(x)->Q(x) impli 5 7. (Exist x)P(x)->(All x)Q(x) |- (All x)(P(x)->Q(x)) ai 6 第19关：6.1节第2题h) 任务描述不用导出规则，请证明：(∀x)(P(x)→Q(x))⊢(∀x)P(x)→(∀x)Q(x)。 Premise: (All x)(P(x)->Q(x)) Conclusion: (All x)P(x)->(All x)Q(x) 1. (All x)(P(x)->Q(x)),(All x)P(x) |- (All x)(P(x)->Q(x)) prem 2. (All x)(P(x)->Q(x)),(All x)P(x) |- P(x)->Q(x) ae 1 (x/x) 3. (All x)(P(x)->Q(x)),(All x)P(x) |- (All x)P(x) prem 4. (All x)(P(x)->Q(x)),(All x)P(x) |- P(x) ae 3 (x/x) 5. (All x)(P(x)->Q(x)),(All x)P(x) |- Q(x) imple 4,2 6. (All x)(P(x)->Q(x)),(All x)P(x) |- (All x)Q(x) ai 5 7. (All x)(P(x)->Q(x)) |- (All x)P(x)->(All x)Q(x) impli 6 第20关：6.1节第3题 任务描述该问题符号化为： 前件：(∀x)(∀y)(R(x,y)−>R(y,x)),(∀x)(∀y)(∀z)(R(x,y)∧R(y,z)→R(x,z)),(∀x)(∃y)R(x,y) 结论：(∀x)R(x,x) 即要用自然推理系统证明：(∀x)(∀y)(R(x,y)−>R(y,x)),(∀x)(∀y)(∀z)(R(x,y)∧R(y,z)→R(x,z)),(∀x)(∃y)R(x,y)⊢(∀x)R(x,x)。 Premise: (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y) Conclusion: (All x)R(x,x) 1. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y) |- (All x)(Exist y)R(x,y) prem 2. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y) |- (Exist y)R(x,y) ae 1 (x/x) 3. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y),R(x,t) |- R(x,t) prem 4. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y),R(x,t) |- (All x)(All y)(R(x,y)->R(y,x)) prem 5. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y),R(x,t) |- (All y)(R(x,y)->R(y,x)) ae 4 (x/x) 6. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y),R(x,t) |- R(x,t)->R(t,x) ae 5 (t/y) 7. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y),R(x,t) |- R(t,x) imple 3,6 8. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y),R(x,t) |- R(x,t)/\R(t,x) andi 3,7 9. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y),R(x,t) |- (Exist y)(R(x,y)/\R(y,x)) ei 8 (t/y) 10. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y) |- (Exist y)(R(x,y)/\R(y,x)) ee 2,9 11. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y),R(x,t)/\R(t,x) |- R(x,t)/\R(t,x) prem 12. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y),R(x,t)/\R(t,x) |- (All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)) prem 13. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y),R(x,t)/\R(t,x) |- (All y)(All z)(R(x,y)/\R(y,z)->R(x,z)) ae 12 (x/x) 14. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y),R(x,t)/\R(t,x) |- (All z)(R(x,t)/\R(t,z)->R(x,z)) ae 13 (t/y) 15. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y),R(x,t)/\R(t,x) |- R(x,t)/\R(t,x)->R(x,x) ae 14 (x/z) 16. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y),R(x,t)/\R(t,x) |- R(x,t)/\R(t,x) prem 17. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y),R(x,t)/\R(t,x) |- R(x,x) imple 15,16 18. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y) |- R(x,x) ee 10,17 19. (All x)(All y)(R(x,y)->R(y,x)),(All x)(All y)(All z)(R(x,y)/\R(y,z)->R(x,z)),(All x)(Exist y)R(x,y) |- (All x)R(x,x) ai 18 第21关：6.2节第1题a) 任务描述用自然推理系统证明：⊢¬(A∧B)↔¬A∨¬B。 Premise: Conclusion: ~(A/\B)(~A\/~B) 1. ~A,~(A/\B) |- ~(A/\B) prem 2. ~A,A/\B |- A/\B prem 3. ~A,A/\B |- A ande 2 4. ~A,A/\B |- ~A prem 5. ~A,A/\B |- ~(A/\B) ne 3,4 6. ~A |- ~(A/\B) preme 1,5 7. ~B,~(A/\B) |- ~(A/\B) prem 8. ~B,A/\B |- A/\B prem 9. ~B,A/\B |- B ande 8 10. ~B,A/\B |- ~B prem 11. ~B,A/\B |- ~(A/\B) ne 9,10 12. ~B |- ~(A/\B) preme 7,11 13. ~A\/~B |- ~(A/\B) ore 6,12 14. ~(A/\B),~(~A\/~B),~A |- ~(~A\/~B) prem 15. ~(A/\B),~(~A\/~B),~A |- ~A prem 16. ~(A/\B),~(~A\/~B),~A |- ~A\/~B ori 15 17. ~(A/\B),~(~A\/~B) |- ~~A ni 14,16 18. ~(A/\B),~(~A\/~B) |- A nne 17 19. ~(A/\B),~(~A\/~B),~B |- ~(~A\/~B) prem 20. ~(A/\B),~(~A\/~B),~B |- ~B prem 21. ~(A/\B),~(~A\/~B),~B |- ~A\/~B ori 20 22. ~(A/\B),~(~A\/~B) |- ~~B ni 19,21 23. ~(A/\B),~(~A\/~B) |- B nne 22 24. ~(A/\B),~(~A\/~B) |- A/\B andi 18,23 25. ~(A/\B),~(~A\/~B) |- ~(A/\B) prem 26. ~(A/\B) |- ~~(~A\/~B) ni 24,25 27. ~(A/\B) |- (~A\/~B) nne 26 28. |- ~(A/\B)(~A\/~B) equivi 13,27 第22关：6.2节第1题b) 任务描述用自然推理系统证明：⊢A∧(B∨C)↔(A∧B)∨(A∧C)。 Premise: Conclusion: A/\(B\/C)(A/\B)\/(A/\C) 1. A/\B |- A/\B prem 2. A/\B |- A ande 1 3. A/\B |- B ande 1 4. A/\B |- B\/C ori 3 5. A/\B |- A/\(B\/C) andi 2,4 6. A/\C |- A/\C prem 7. A/\C |- A ande 6 8. A/\C |- C ande 6 9. A/\C |- B\/C ori 8 10. A/\C |- A/\(B\/C) andi 7,9 11. (A/\B)\/(A/\C) |- A/\(B\/C) ore 5,10 12. A/\(B\/C),B |- B prem 13. A/\(B\/C),B |- A/\(B\/C) prem 14. A/\(B\/C),B |- A ande 13 15. A/\(B\/C),B |- A/\B andi 12,14 16. A/\(B\/C),B |- (A/\B)\/(A/\C) ori 15 17. A/\(B\/C),~B |- A/\(B\/C) prem 18. A/\(B\/C),~B |- A ande 17 19. A/\(B\/C),~B |- B\/C ande 17 20. B,~(~B/\~C) |- ~(~B/\~C) prem 21. B,~B/\~C |- ~B/\~C prem 22. B,~B/\~C |- ~B ande 21 23. B,~B/\~C |- B prem 24. B,~B/\~C |- ~(~B/\~C) ne 22,23 25. B |- ~(~B/\~C) preme 20,24 26. C,~(~B/\~C) |- ~(~B/\~C) prem 27. C,~B/\~C |- ~B/\~C prem 28. C,~B/\~C |- ~C ande 27 29. C,~B/\~C |- C prem 30. C,~B/\~C |- ~(~B/\~C) ne 28,29 31. C |- ~(~B/\~C) preme 26,30 32. B\/C |- ~(~B/\~C) ore 25,31 33. |- (B\/C)->~(~B/\~C) impli 32 34. A/\(B\/C),~B,~C |- ~B prem 35. A/\(B\/C),~B,~C |- ~C prem 36. A/\(B\/C),~B,~C |- ~B/\~C andi 34,35 37. A/\(B\/C),~B,~C |- B\/C premi 19 38. A/\(B\/C) |- (B\/C)->~(~B/\~C) premi 33 39. A/\(B\/C),~B |- (B\/C)->~(~B/\~C) premi 38 40. A/\(B\/C),~B,~C |- (B\/C)->~(~B/\~C) premi 39 41. A/\(B\/C),~B,~C |- ~(~B/\~C) imple 37,40 42. A/\(B\/C),~B |- ~~C ni 36,41 43. A/\(B\/C),~B |- C nne 42 44. A/\(B\/C),~B |- A/\C andi 43,18 45. A/\(B\/C),~B |- (A/\B)\/(A/\C) ori 44 46. A/\(B\/C) |- (A/\B)\/(A/\C) preme 45,16 47. |- A/\(B\/C)(A/\B)\/(A/\C) equivi 46,11 第23关：6.2节第1题c) 任务描述用自然推理系统证明：⊢A∨(B∧C)↔(A∨B)∧(A∨C)。 可使用的导出规则： 1.¬A∨¬B⊢¬(A∧B) 2.¬A∧¬B⊢¬(A∨B) Premise: Conclusion: A\/(B/\C)(A\/B)/\(A\/C) 1. A |- A prem 2. A |- A\/B ori 1 3. A |- A\/C ori 1 4. A |- (A\/B)/\(A\/C) andi 2,3 5. B/\C |- B/\C prem 6. B/\C |- B ande 5 7. B/\C |- A\/B ori 6 8. B/\C |- C ande 5 9. B/\C |- A\/C ori 8 10. B/\C |- (A\/B)/\(A\/C) andi 7,9 11. A\/(B/\C) |- (A\/B)/\(A\/C) ore 4,10 12. (A\/B)/\(A\/C),A |- A prem 13. (A\/B)/\(A\/C),A |- A\/(B/\C) ori 12 14. (A\/B)/\(A\/C),~A,~B |- (A\/B)/\(A\/C) prem 15. (A\/B)/\(A\/C),~A,~B |- A\/B ande 14 16. (A\/B)/\(A\/C),~A,~B |- ~(A\/B) dr 17. (A\/B)/\(A\/C),~A |- ~~B ni 15,16 18. (A\/B)/\(A\/C),~A |- B nne 17 19. (A\/B)/\(A\/C),~A,~C |- (A\/B)/\(A\/C) prem 20. (A\/B)/\(A\/C),~A,~C |- A\/C ande 19 21. (A\/B)/\(A\/C),~A,~C |- ~(A\/C) dr 22. (A\/B)/\(A\/C),~A |- ~~C ni 20,21 23. (A\/B)/\(A\/C),~A |- C nne 22 24. (A\/B)/\(A\/C),~A |- B/\C andi 23,18 25. (A\/B)/\(A\/C),~A |- A\/(B/\C) ori 24 26. (A\/B)/\(A\/C) |- A\/(B/\C) preme 13,25 27. |- A\/(B/\C)(A\/B)/\(A\/C) equivi 26,11 第24关：6.2节第1题d) 任务描述任务描述 用自然推理系统证明：⊢A∨F↔A。 Premise: Conclusion: A\/FA 1. A\/F |- A dr 2. A |- A\/F dr 3. |- A\/FA equivi 1,2 第25关：6.2节第1题e) 任务描述用自然推理系统证明：⊢A∧T↔A。 Premise: Conclusion: A/\TA 1. A/\T |- A dr 2. A |- A/\T dr 3. |- A/\TA equivi 1,2 第26关：6.2节第1题f) 任务描述用自然推理系统证明：⊢(A→B)↔(¬A∨B)。 Premise: Conclusion: (A->B)~A\/B 1. (A->B) |- ~A\/B dr 2. ~A\/B |- (A->B) dr 3. |- (A->B)~A\/B equivi 1,2 第27关：6.2节第2题g) 任务描述用自然推理系统证明：¬(A→B)⊢A Premise: ~(A->B) Conclusion: A 1. ~(A->B) |- A/\A dr 2. ~(A->B) |- A ande 1 第28关：6.2节第1题h) 任务描述用自然推理系统证明：¬(A→B)⊢¬B。 Premise: ~(A->B) Conclusion: ~B 1. ~(A->B) |- ~(~A\/B) dr 2. ~(A->B) |- A/\~B dr 3. ~(A->B) |- ~B ande 2 第29关：6.2节第2题a) 任务描述用自然推理系统证明：⊢(∃x)(C→P(x))↔(C→(∃x)P(x))。 可以使用的导出规则有： 1.¬(A→B)⊢A∧¬B 2.(∀x)(¬P(x))⊢¬(∃x)P(x) 3.¬(∃x)P(x)⊢(∀x)(¬P(x)) Premise: Conclusion: ((Exist x)(C->P(x)))(C->(Exist x)P(x)) 1. C->P(x),C |- C->P(x) prem 2. C->P(x),C |- C prem 3. C->P(x),C |- P(x) imple 1,2 4. C->P(x),C |- (Exist x)P(x) ei 3 (x/x) 5. C->P(x) |- C->(Exist x)P(x) impli 4 6. (Exist x)(C->P(x)) |- C->(Exist x)P(x) lei 5 7. C->(Exist x)P(x),C |- C->(Exist x)P(x) prem 8. C->(Exist x)P(x),C |- C prem 9. C->(Exist x)P(x),C |- (Exist x)P(x) imple 7,8 10. C->(Exist x)P(x),C,P(t) |- (Exist x)(C->P(x)) dr 11. C->(Exist x)P(x),C |- (Exist x)(C->P(x)) ee 9,10 12. C->(Exist x)P(x),~C |- (Exist x)(C->P(x)) dr 13. C->(Exist x)P(x) |- (Exist x)(C->P(x)) preme 11,12 14. |- ((Exist x)(C->P(x)))(C->(Exist x)P(x)) equivi 6,13 第30关：6.2节第2题b)-1 任务描述用自然推理系统证明：(∃x)(P(x)→C)⊢(∀x)P(x)→C。 Premise: (Exist x)(P(x)->C) Conclusion: (All x)P(x)->C 1. P(t)->C |- P(t)->C prem 2. P(t)->C,P(t) |- C dr 3. (All x)P(x) |- P(t)->C->C dr 5. P(t)->C |- (All x)P(x)->C dr 6. (Exist x)(P(x)->C) |- (Exist x)(P(x)->C) prem 7. (Exist x)(P(x)->C),P(t)->C |- P(t)->C prem 8. (Exist x)(P(x)->C),(P(t)->C) |- (All x)P(x)->C dr 9. (P(x)->C) |- (All x)P(x)->C dr 10. (Exist x)(P(x)->C) |- (All x)P(x)->C lei 9 第31关：6.2节第2题b)-2 任务描述用自然推理系统证明：(∀x)P(x)→C⊢(∃x)(P(x)→C)。 可以使用的导出规则： 1.¬(A→B)⊢A∧¬B 2.¬(∃x)P(x)⊢(∀x)(¬P(x)) Premise: (All x)P(x)->C Conclusion: (Exist x)(P(x)->C) 1. (All x)P(x)->C |- (All x)P(x)->C prem 2. (All x)P(x)->C |- P(t)->C dr 3. (All x)P(x)->C |- (Exist x)(P(x)->C) ei 2 (t/x) 第32关：6.2节第2题c)-1 任务描述用自然推理系统证明：(∃x)(P(x)∨C)⊢(∃x)P(x)∨C。 Premise: (Exist x)(P(x)\/C) Conclusion: (Exist x)P(x)\/C 1. P(x) |- P(x) prem 2. P(x) |- (Exist x)P(x) ei 1 (x/x) 3. P(x) |- (Exist x)P(x)\/C ori 2 4. C |- C prem 5. C |- (Exist x)P(x)\/C ori 4 6. P(x)\/C |- (Exist x)P(x)\/C ore 3,5 7. (Exist x)(P(x)\/C) |- (Exist x)P(x)\/C lei 6 第33关：6.2节第2题c)-2 任务描述用自然推理系统证明：(∃x)P(x)∨C⊢(∃x)(P(x)∨C)。 Premise: (Exist x)P(x)\/C Conclusion: (Exist x)(P(x)\/C) 1. (Exist x)P(x) |- (Exist x)P(x) prem 2. (Exist x)P(x),P(t) |- P(t) prem 3. (Exist x)P(x),P(t) |- P(t)\/C ori 2 4. (Exist x)P(x),P(t) |- (Exist x)(P(x)\/C) ei 3 (t/x) 5. (Exist x)P(x) |- (Exist x)(P(x)\/C) dr 6. C |- C prem 7. C |- P(x)\/C ori 6 8. C |- (Exist x)(P(x)\/C) ei 7 (x/x) 9. (Exist x)P(x)\/C |- (Exist x)(P(x)\/C) ore 5,8 第34关：6.2节第2题d)-1 任务描述用自然推理系统证明：(∀x)(P(x)∧C)⊢(∀x)P(x)∧C。 Premise: (All x)(P(x)/\C) Conclusion: (All x)P(x)/\C 1. P(x)/\C |- P(x)/\C prem 2. P(x)/\C |- P(x) ande 1 3. P(x)/\C |- C ande 1 4. (All x)(P(x)/\C) |- (All x)P(x) aai 2 5. (All x)(P(x)/\C) |- C lai 3 6. (All x)(P(x)/\C) |- (All x)P(x)/\C andi 4,5 第35关：6.2节第2题d)-2 任务描述用自然推理系统证明：(∀x)P(x)∧C⊢(∀x)(P(x)∧C)。 Premise: (All x)P(x)/\C Conclusion: (All x)(P(x)/\C) 1. (All x)P(x)/\C |- (All x)P(x)/\C prem 2. (All x)P(x)/\C |- (All x)P(x) ande 1 3. (All x)P(x)/\C |- P(x) ae 2 (x/x) 4. (All x)P(x)/\C |- C ande 1 5. (All x)P(x)/\C |- P(x)/\C andi 3,4 6. (All x)P(x)/\C |- (All x)(P(x)/\C) ai 5 第36关：6.2节第2题e)-1 任务描述用自然推理系统证明：¬(∀x)P(x)⊢(∃x)¬P(x)。 Premise: ~(All x)P(x) Conclusion: (Exist x)(~P(x)) 1. ~(All x)P(x),~(Exist x)(~P(x)),~P(x) |- ~P(x) prem 2. ~(All x)P(x),~(Exist x)(~P(x)),~P(x) |- (Exist x)(~P(x)) ei 1 (x/x) 3. ~(All x)P(x),~(Exist x)(~P(x)),~P(x) |- ~(Exist x)(~P(x)) prem 4. ~(All x)P(x),~(Exist x)(~P(x)) |- ~~P(x) ni 2,3 5. ~(All x)P(x),~(Exist x)(~P(x)) |- P(x) nne 4 6. ~(All x)P(x),~(Exist x)(~P(x)) |- (All x)P(x) ai 5 7. ~(All x)P(x),~(Exist x)(~P(x)) |- ~(All x)P(x) prem 8. ~(All x)P(x) |- ~~(Exist x)(~P(x)) ni 6,7 9. ~(All x)P(x) |- (Exist x)(~P(x)) nne 8 第37关：6.2节第2题e)-2 任务描述用自然推理系统证明：(∃x)¬P(x)⊢¬(∀x)P(x)。 Premise: ~(All x)P(x) Conclusion: (Exist x)(~P(x)) 1. ~(All x)P(x),~(Exist x)(~P(x)),~P(x) |- ~P(x) prem 2. ~(All x)P(x),~(Exist x)(~P(x)),~P(x) |- (Exist x)(~P(x)) ei 1 (x/x) 3. ~(All x)P(x),~(Exist x)(~P(x)),~P(x) |- ~(Exist x)(~P(x)) prem 4. ~(All x)P(x),~(Exist x)(~P(x)) |- ~~P(x) ni 2,3 5. ~(All x)P(x),~(Exist x)(~P(x)) |- P(x) nne 4 6. ~(All x)P(x),~(Exist x)(~P(x)) |- (All x)P(x) ai 5 7. ~(All x)P(x),~(Exist x)(~P(x)) |- ~(All x)P(x) prem 8. ~(All x)P(x) |- ~~(Exist x)(~P(x)) ni 6,7 9. ~(All x)P(x) |- (Exist x)(~P(x)) nne 8 第38关：6.2节第2题f) 任务描述用自然推理系统证明：(∃x)(P(x)∧Q(x))⊢(∃x)P(x)∧(∃x)Q(x)。 Premise: (Exist x)(P(x)/\Q(x)) Conclusion: (Exist x)P(x)/\(Exist x)Q(x) 1. P(x)/\Q(x) |- P(x)/\Q(x) prem 2. P(x)/\Q(x) |- P(x) ande 1 3. (Exist x)(P(x)/\Q(x)) |- (Exist x)P(x) eei 2 4. P(x)/\Q(x) |- Q(x) ande 1 5. (Exist x)(P(x)/\Q(x)) |- (Exist x)Q(x) eei 4 6. (Exist x)(P(x)/\Q(x)) |- (Exist x)P(x)/\(Exist x)Q(x) andi 3,5 PS：要了解逻辑基础，可以类比为学语文要学拼音。逻辑有一些基本概念和规则，比如命题逻辑和谓词逻辑中的连接词、量词等，这些都是需要掌握的。 学习推理规则很重要。自然推理系统常用的推理规则，比如假言推理、析取引入与消除、合取引入与消除、否定引入与消除等，这些都需要熟悉。练习推理技巧。就像打dota需要不断练习一样，多做一些推理问题的练习，尝试使用自然推理系统进行推导，并检查推导的正确性。逐步增加难度，挑战更复杂的推理问题。 对于这部分内容，持续学习和提升是关键。像追番一样保持好奇心，关注新的推理问题和技巧，多推多练，不断提高自然推理的能力。 反正这门课对于 6yuan or 6dd 牛马们来说比较好通过，实在弄不懂，抄就完了。 （￣︶￣）↗ （就没听说过挂离散的(～￣▽￣)～） |
【本文地址】
公司简介
联系我们