Skip to content Skip to navigation

Connexions

You are here: Home » Content » Comp280 hw02 solution

Navigation

Content Actions
  • Download module PDF
  • Add to ...
    Add the module to:
    • My Favorites
    • A lens
    • An external social bookmarking service
    • My Favorites (What is 'My Favorites'?)
      'My Favorites' is a special kind of lens which you can use to bookmark modules and collections directly in Connexions. 'My Favorites' can only be seen by you, and collections saved in 'My Favorites' can remember the last module you were on. You need a Connexions account to use 'My Favorites'.
    • A lens (What is a lens?)

      Definition of a lens

      Lenses

      A lens is a custom view of Connexions content. You can think of it as a fancy kind of list that will let you see Connexions through the eyes of organizations and people you trust.

      What is in a lens?

      Lens makers point to Connexions materials (modules and collections), creating a guide that includes their own comments and descriptive tags about the content.

      Who can create a lens?

      Any individual Connexions member, a community, or a respected organization.

    • External bookmarks
  • E-mail the author

Recently Viewed

This feature requires Javascript to be enabled.

Comp280 hw02 solution

Module by: Ian Barland

Summary: Solutions for 2004.spring comp280 hw02.

All (non-practice, non-extra-credit) problems due 2004.Feb.03 (Tue) 17:00.

aside:

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.

Reasoning with Inference Rules

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.

Exercise 1

N.B.:

(Carried over from original hw01 assignment.)

(2 pts.) Fill in the blank reasons in the following proof that ∨∨ commutes, that is, χ ∨ υ ⊢ υ ∨ χχ ∨ υ ⊢ υ ∨ χ.

1χ ∨ υχ ∨ υ  premise
2subproof:χ ⊢ υ ∨ χχ ⊢ υ ∨ χ  
2.a  χχ premise for subproof
2.b  υ ∨ χυ ∨ χ ∨∨Intro
3subproof:υ ⊢ υ ∨ χυ ⊢ υ ∨ χ  
3.a  υυ premise for subproof
3.b  υ ∨ χυ ∨ χ ____________
4υ ∨ χυ ∨ χ  ____________

Solution 1

  • Line 3b justification: ∨∨Intro, by line 3a.
  • Line 4 justification: ∨∨Elim, by lines 1,2,3, where φφ=χχ and ψψ=υυ and θθ=υ ∨ χυ ∨ χ

Exercise 2

(5pts.) Show that τ ∧ χτ → υχ → ω ⊢ υ ∧ ωτ ∧ χτ → υχ → ω ⊢ υ ∧ ω. (It may take around 8 steps.)

Solution 2

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 ψψ=ωω

Exercise 3

(4pts) Using the inference rule RAA, prove ¬χ ⊢ ¬χ ∧ υ¬χ ⊢ ¬χ ∧ υ.

Solution 3

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
2subproof:¬¬χ ∧ υ ⊢ 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 φφ=¬χ ∧ υ¬χ ∧ υ

Exercise 4

(6pts.) Show that ¬W-safe ∨ ¬Y-unsafe ⊢ W-unsafe ∨ Y-safe¬W-safe ∨ ¬Y-unsafe ⊢ W-unsafe ∨ Y-safe.

hint:

Use the ∨∨Elim inference rule to get the final result.

Solution 4

1¬W-safe ∨ ¬Y-unsafe¬W-safe ∨ ¬Y-unsafe  premise
2subproof:¬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-unsafeWaterWorld domain axiom
2.c  W-unsafeW-unsafe →→Elim
2.d  W-unsafe ∨ Y-safeW-unsafe ∨ Y-safe ∨∨Intro
3subproof:¬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
4W-unsafe ∨ Y-safeW-unsafe ∨ Y-safe  ∨∨Elim

Exercise 5

(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:

1X-has-1X-has-1  ____________
2____________  WaterWorld domain axiom
3____________  →→Elim
4subproof: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 ____________
5subproof:¬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 ____________
6W-safe ∧ Y-unsafe ∨ ¬W-safe ∧ Y-unsafeW-safe ∧ Y-unsafe ∨ ¬W-safe ∧ Y-unsafe From class, φ ∨ ¬φφ ∨ ¬φ, with φ____________φ____________
7W-unsafe ∨ Y-unsafeW-unsafe ∨ Y-unsafe  ____________

Solution 5

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) φ ∨ ¬φφ ∨ ¬φ.

1X-has-1X-has-1  premise
2X-has-1 → W-safe ∧ Y-unsafe ∨ W-unsafe ∧ Y-safeX-has-1 → W-safe ∧ Y-unsafe ∨ W-unsafe ∧ Y-safe  WaterWorld domain axiom
3W-safe ∧ Y-unsafe ∨ W-unsafe ∧ Y-safeW-safe ∧ Y-unsafe ∨ W-unsafe ∧ Y-safe  →→Elim
4subproof: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
5subproof:¬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
6W-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
7W-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

Exercise 6

[practice; 0pts]

Figure 1: A sample WaterWorld board
Figure 1 (hwA-1.png)

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.

Solution 6

1Q-has-1Q-has-1  premise
2X-has-1X-has-1  premise
3¬Y-unsafe¬Y-unsafe  premise
4