All (non-practice, non-extra-credit) problems
due 2004.Feb.03 (Tue) 17:00.
Rice Students: If you like, you can play WaterWorld
on OwlNet, in /home/comp280/bin/waterworld.
To run Waterworld on your home computer,
download (from owlnet) the directory
/home/scheme/plt/205/collects/waterworld/,
and (from drscheme) add it as a teachpack.
For proofs on this homework,
Remember that each step must be justified by
one of:
"premise",
a listed
inference rule (.ps)
(a previous line number and, if ambiguous,
substitutions for the inference rule's metavariables),
or a
WaterWorld domain axiom.
(Carried over from original hw01 assignment.)
(2 pts.)
Fill in the blank reasons in the following proof that ∨∨ commutes,
that is, χ ∨ υ ⊢ υ ∨ χχ ∨ υ ⊢ υ ∨ χ.
| 1 | χ ∨ υχ ∨ υ | | premise
|
| 2 | subproof:χ ⊢ υ ∨ χχ ⊢ υ ∨ χ | | |
| 2.a | | χχ | premise for subproof
|
| 2.b | | υ ∨ χυ ∨ χ | ∨∨Intro
|
| 3 | subproof:υ ⊢ υ ∨ χυ ⊢ υ ∨ χ | | |
| 3.a | | υυ | premise for subproof
|
| 3.b | | υ ∨ χυ ∨ χ | ____________
|
| 4 | υ ∨ χυ ∨ χ | | ____________
|
-
Line 3b justification: ∨∨Intro, by line 3a.
-
Line 4 justification:
∨∨Elim,
by lines 1,2,3,
where φφ=χχ
and ψψ=υυ
and θθ=υ ∨ χυ ∨ χ
(5pts.)
Show that
τ ∧ χτ → υχ → ω ⊢ υ ∧ ωτ ∧ χτ → υχ → ω ⊢ υ ∧ ω. (It may take around 8 steps.)
This is basically just two instances of →→Elim, plus
a little manipulation of ∧∧.
| 1 | τ ∧ χτ ∧ χ | premise
|
| 2 | ττ | ∧∧Elim (left),
by line 1,
where φφ=ττ
and ψψ=χχ
|
| 3 | τ → υτ → υ | premise
|
| 4 | υυ | →→Elim,
by lines 2,3,
where φφ=ττ
and ψψ=υυ
|
| 5 | χχ | ∧∧Elim (right),
by line 1,
where φφ=ττ
and ψψ=χχ
|
| 6 | χ → ωχ → ω | premise
|
| 7 | ωω | →→Elim,
by lines 5,6,
where φφ=χχ
and ψψ=ωω
|
| 8 | υ ∧ ωυ ∧ ω | ∧∧Intro,
by lines 4,7,
where φφ=υυ
and ψψ=ωω
|
(4pts)
Using the inference rule RAA, prove
¬χ ⊢ ¬χ ∧ υ¬χ ⊢ ¬χ ∧ υ.
We observe that to use RAA to conclude
¬χ ∧ υ¬χ ∧ υ
will require a subproof of
¬¬χ ∧ υ ⊢ false¬¬χ ∧ υ ⊢ .
(That is, the rule's φφ refers to a WFF which is already a negation:
"¬χ ∧ υ¬χ ∧ υ". Not a problem at all.)
| 1 | ¬χ¬χ | | premise
|
| 2 | subproof:¬¬χ ∧ υ ⊢ false¬¬χ ∧ υ ⊢ | | |
| 2.a | | ¬¬χ ∧ υ¬¬χ ∧ υ | premise for subproof
|
| 2.b | | χ ∧ υχ ∧ υ | ¬¬Elim,
by line 2.1
|
| 2.c | | χχ | ∧∧Elim,
by line 2.2
|
| 2.d | | false | falseIntro,
by lines 1,2.3
|
| 3 | ¬χ ∧ υ¬χ ∧ υ | | RAA,
by line 2,
where φφ=¬χ ∧ υ¬χ ∧ υ
|
(6pts.)
Show that
¬W-safe ∨ ¬Y-unsafe ⊢ W-unsafe ∨ Y-safe¬W-safe ∨ ¬Y-unsafe ⊢ W-unsafe ∨ Y-safe.
Use the ∨∨Elim inference rule to get the final result.
| 1 | ¬W-safe ∨ ¬Y-unsafe¬W-safe ∨ ¬Y-unsafe | | premise
|
| 2 | subproof:¬W-safe ⊢ W-unsafe ∨ Y-safe¬W-safe ⊢ W-unsafe ∨ Y-safe | | |
| 2.a | | ¬W-safe¬W-safe | premise for subproof
|
| 2.b | | ¬W-safe → W-unsafe¬W-safe → W-unsafe | WaterWorld domain axiom
|
| 2.c | | W-unsafeW-unsafe | →→Elim
|
| 2.d | | W-unsafe ∨ Y-safeW-unsafe ∨ Y-safe | ∨∨Intro
|
| 3 | subproof:¬Y-unsafe ⊢ W-unsafe ∨ Y-safe¬Y-unsafe ⊢ W-unsafe ∨ Y-safe | | |
| 3.a | | ¬Y-unsafe¬Y-unsafe | premise for subproof
|
| 3.b | | ¬Y-unsafe → Y-safe¬Y-unsafe → Y-safe | WaterWorld domain axiom
|
| 3.c | | Y-safeY-safe | →→Elim
|
| 3.d | | W-unsafe ∨ Y-safeW-unsafe ∨ Y-safe | ∨∨Intro
|
| 4 | W-unsafe ∨ Y-safeW-unsafe ∨ Y-safe | | ∨∨Elim
|
(5pts)
For the following WaterWorld proof of
X-has-1 ⊢ W-unsafe ∨ Y-unsafeX-has-1 ⊢ W-unsafe ∨ Y-unsafe,
provide the missing steps and/or reasons:
| 1 | X-has-1X-has-1 | | ____________
|
| 2 | ____________ | | WaterWorld domain axiom
|
| 3 | ____________ | | →→Elim
|
| 4 | subproof:W-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafeW-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafe | | |
| 4.a | | W-safe ∧ Y-unsafeW-safe ∧ Y-unsafe | premise for subproof
|
| 4.b | | Y-unsafeY-unsafe | ____________
|
| 4.c | | W-unsafe ∨ Y-unsafeW-unsafe ∨ Y-unsafe | ____________
|
| 5 | subproof:¬W-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafe¬W-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafe | | |
| 5.a | | ¬W-safe ∧ Y-unsafe¬W-safe ∧ Y-unsafe | premise for subproof
|
| 5.b | | W-unsafe ∧ Y-safeW-unsafe ∧ Y-safe | CaseElim (left),
where φφ=____________,
and ψψ=____________.
|
| 5.c | | ____________ | ____________
|
| 5.d | | W-unsafe ∨ Y-unsafeW-unsafe ∨ Y-unsafe | ____________
|
| 6 | W-safe ∧ Y-unsafe ∨ ¬W-safe ∧ Y-unsafeW-safe ∧ Y-unsafe ∨ ¬W-safe ∧ Y-unsafe | | From class, φ ∨ ¬φφ ∨ ¬φ,
with φ____________φ____________
|
| 7 | W-unsafe ∨ Y-unsafeW-unsafe ∨ Y-unsafe | | ____________
|
Since Step 4 is of the form φ → θφ → θ, and
Step 5 is of the form ¬φ → θ¬φ → θ,
this is enough to prove θθ by ∨∨Elim,
once we include (from class) φ ∨ ¬φφ ∨ ¬φ.
| 1 | X-has-1X-has-1 | | premise
|
| 2 | X-has-1 → W-safe ∧ Y-unsafe ∨ W-unsafe ∧ Y-safeX-has-1 → W-safe ∧ Y-unsafe ∨ W-unsafe ∧ Y-safe | | WaterWorld domain axiom
|
| 3 | W-safe ∧ Y-unsafe ∨ W-unsafe ∧ Y-safeW-safe ∧ Y-unsafe ∨ W-unsafe ∧ Y-safe | | →→Elim
|
| 4 | subproof:W-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafeW-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafe | | |
| 4.a | | W-safe ∧ Y-unsafeW-safe ∧ Y-unsafe | premise for subproof
|
| 4.b | | Y-unsafeY-unsafe | ∧∧Elim
|
| 4.c | | W-unsafe ∨ Y-unsafeW-unsafe ∨ Y-unsafe | ∨∨Intro
|
| 5 | subproof:¬W-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafe¬W-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafe | | |
| 5.a | | ¬W-safe ∧ Y-unsafe¬W-safe ∧ Y-unsafe | premise for subproof
|
| 5.b | | W-unsafe ∧ Y-safeW-unsafe ∧ Y-safe | CaseElim (left),
where φφ=W-safe ∧ Y-unsafeW-safe ∧ Y-unsafe,
and ψψ=W-unsafe ∧ Y-safeW-unsafe ∧ Y-safe
|
| 5.c | | W-unsafeW-unsafe | ∧∧Elim
|
| 5.d | | W-unsafe ∨ Y-unsafeW-unsafe ∨ Y-unsafe | ∨∨Intro
|
| 6 | W-safe ∧ Y-unsafe ∨ ¬W-safe ∧ Y-unsafeW-safe ∧ Y-unsafe ∨ ¬W-safe ∧ Y-unsafe | | From class, φ ∨ ¬φφ ∨ ¬φ,
with φW-safe ∧ Y-unsafeφW-safe ∧ Y-unsafe
|
| 7 | W-unsafe ∨ Y-unsafeW-unsafe ∨ Y-unsafe | | ∨∨Elim,
by lines 5,6, with
φW-safe ∧ Y-unsafe
ψ¬W-safe ∧ Y-unsafe
θW-unsafe ∨ Y-unsafeφW-safe ∧ Y-unsafeψ¬W-safe ∧ Y-unsafeθW-unsafe ∨ Y-unsafe
|
[practice; 0pts]
Given the
above figure, and using any of the immediately obvious facts
as premises, prove that location P is safe
by using our proof system and the WaterWorld domain axioms.
While this proof is longer (nearly 30 steps),
it's not too bad. To make life easier,
you may also use the following:
- ¬φ ⊢ ¬φ ∧ ψ¬φ ⊢ ¬φ ∧ ψ
- Q-has-1 → P-safe ∧ R-safe ∨ P-safe ∧ W-safe ∨ R-safe ∧ W-safeQ-has-1 → P-safe ∧ R-safe ∨ P-safe ∧ W-safe ∨ R-safe ∧ W-safe.
- Not only is Y-safeY-safe an allowable premise
(reading off the given board),
but so is ¬Y-unsafe¬Y-unsafe.
| 1 | Q-has-1Q-has-1 | | premise
|
| 2 | X-has-1X-has-1 | | premise
|
| 3 | ¬Y-unsafe¬Y-unsafe | | premise
|
| 4 | |