Download Read the Stdm User Manual

> p82 = -- Q |- (P => P&Q)
>
ImpI (AndI (Assume P, Assume Q)
>
(And P Q))
>
(Imp P (And P Q))
> p83 = -|- Q => (P => (P&Q))
>
ImpI (ImpI (AndI (Assume P, Assume Q)
>
(And P Q))
>
(Imp P (And P Q)))
>
(Imp Q (Imp P (And P Q)))
Valid proofs with Imp Elimination
> p9 = ImpE (Assume P, Assume (Imp P Q))
>
Q
Here is the theorem and proofs that are used in the book; run them like this:
check_proof example_theorem proof1
check_proof example_theorem proof2
(should be valid)
(should give error message)
> example_theorem :: Theorem
> example_theorem =
>
Theorem
>
[]
>
(Imp Q (Imp (And P R) (And R Q)))
> proof1 =
>
ImpI
>
(ImpI
>
(AndI
>
((AndER
>
(Assume (And P R))
>
R),
>
Assume Q)
>
(And R Q))
>
(Imp (And P R) (And R Q)))
>
(Imp Q (Imp (And P R) (And R Q)))
The following proof is incorrect proof, because QR was inferred where RQ was needed.
> proof2 =
>
ImpI
>
(ImpI
>
(AndI
>
(Assume Q,
>
(AndER
>
(Assume (And P R))
>
R))
>
(And R Q))
>
(Imp (And P R) (And R Q)))
>
(Imp Q (Imp (And P R) (And R Q)))
16