代码之家 › 专栏 › 技术社区 › Gergely

命题逻辑的格区分

isabelle logic

Gergely · 技术社区 · 9 年前

我想证明

P ==> P

通过案例区分来理解后者。

lemma "P â¹ P"
proof (cases P)

goal (2 subgoals):
1. P â¹ P â¹ P
2. P â¹ Â¬ P â¹ P

我不太确定我是否想要这些。我想假设P是真的,然后通过假设证明P是真,然后假设不是P,并通过假设证明不是P。就像在真相表中一样。

第二个子目标中的非P似乎很奇怪,这是可证明的吗?

 assume P then show P by assumption

 Successful attempt to solve goal by exported rule:
 (P) â¹ P 

next

goal (1 subgoal):
 1. P â¹ Â¬ P â¹ P

 assume P assume "Â¬P" then show "Â¬P" by (rule HOL.FalseE)

这一切都糟透了。

我怎样才能把P而不是P作为案例?

1 回复 | 直到 9 年前

Ben Keks 9 年前

P而不是P 是你的案子。如果你写“案例P”,Isabelle复制当前目标,并将P添加到第一个子目标的假设中,将P添加至第二个子目标的假定中。如果以这种方式使用,目标的右侧不受case方法的影响。

在您的案例中,您不必证明第二个子目标中的P,但可以将其用作案例目的地引入的附加假设。

很显然,你无法从第二个子目标中的P证明P。幸运的是,全局假设P仍然存在,因此这两种情况仍然证明P来自P,这与没有案例目的地的情况一样是真实的;)。

如果你想通过让Isabelle直接插入变量的可能值来证明什么,你可以尝试:

  lemma "P â¹ P"
  proof (induct P) 

  goal (2 subgoals):
  1. True â¹ True
  2. False â¹ False

推荐文章

Wadu Hek · 查找列表中唯一的重复项

2 年前

Johan Klemantan · 带条件的嵌套循环中的lambda

2 年前

Sudhanva c · 如何提高编码技能?[已关闭]

7 年前

Arie Wijaya · 无法将伪代码转换为java[已关闭]

7 年前

Gauthaman Sahadevan · 回答这个调度算法场景的最佳方式是什么?

7 年前

Adrian DSouza · python中逻辑语句的组合(and、or)

7 年前

Adrian Rotama · 将十进制四舍五入到最接近的十次方的轨道

7 年前

MMMMMCK · Pthreads:为pthread\u cond\u wait使用While循环背后的逻辑

7 年前

Sawbonz · 为什么If语句不适用于Python和Pygame

7 年前

Kevin · 根据第一个组合框中插入的数字生成组合框

7 年前