命题逻辑答案

【问题标题】：Propositional logic [closed]命题逻辑
【发布时间】：2015-06-06 05:41:23
【问题描述】：

我正在尝试从(p→q) and (qr→s) 到(pr→s)，这与((not p) or q) and (not(q and r) or s) 到(not(p and r) or s) 相同

【问题讨论】：

也许你会澄清这是一个编程问题。这看起来应该在Mathematics
其实看起来更像是作业

【解决方案1】：

定理：

   p → q
= ¬p ∨ q       -- 1

   (q ∧ r) → s
= ¬(q ∧ r) ∨ s
=  ¬q ∨ ¬r ∨ s -- 2

   ¬p ∨ ¬r ∨ s -- from 1 and 2, q and ¬q cancel
= ¬(p ∧ r) ∨ s
=  (p ∧ r) → s

Qed。

使用 Coq，我们可以证明这个定理如下：

Coq < Theorem prop : forall p q r s : Prop, (p -> q) /\ (q /\ r -> s) -> p /\ r -> s.
1 subgoal

  ============================
   forall p q r s : Prop, (p -> q) /\ (q /\ r -> s) -> p /\ r -> s

prop < intros.
1 subgoal

  p : Prop
  q : Prop
  r : Prop
  s : Prop
  H : (p -> q) /\ (q /\ r -> s)
  H0 : p /\ r
  ============================
   s

prop < destruct H.
1 subgoal

  p : Prop
  q : Prop
  r : Prop
  s : Prop
  H : p -> q
  H1 : q /\ r -> s
  H0 : p /\ r
  ============================
   s

prop < destruct H0.
1 subgoal

  p : Prop
  q : Prop
  r : Prop
  s : Prop
  H : p -> q
  H1 : q /\ r -> s
  H0 : p
  H2 : r
  ============================
   s

prop < apply H1.
1 subgoal

  p : Prop
  q : Prop
  r : Prop
  s : Prop
  H : p -> q
  H1 : q /\ r -> s
  H0 : p
  H2 : r
  ============================
   q /\ r

prop < split.
2 subgoals

  p : Prop
  q : Prop
  r : Prop
  s : Prop
  H : p -> q
  H1 : q /\ r -> s
  H0 : p
  H2 : r
  ============================
   q

subgoal 2 is:
 r

prop < exact (H H0).
1 subgoal

  p : Prop
  q : Prop
  r : Prop
  s : Prop
  H : p -> q
  H1 : q /\ r -> s
  H0 : p
  H2 : r
  ============================
   r

prop < exact H2.
No more subgoals.

prop < Qed.
intros.
destruct H.
destruct H0.
apply H1.
split.
 exact (H H0).

 exact H2.

prop is defined

希望对您有所帮助。

【讨论】：