这是一篇来自澳洲的关于计算机基础相关的作业代写

1 New Connective (1) (Supp)

Define the connective ˛ via the following truth table:

p q p ˛ q

F F T

F T T

T F T

T T F

For each of the formulae in (1) to (3) below, select:

• ‘tautology’, if the formula is a tautology,
• ‘contradiction’ , if the formula is a contradiction, or
• a situation in which the formula evaluates to False, if it’s a contingency.

There might be more than one true answer. You need to select only one of them.

1. pp ˛ qq ˛ p. Options

• Tautology.
• Contradiction.
• Contigency, and evaluates to F for p “ F and q “ T.
• Contigency, and evaluates to F for p “ T and q “ F.
• Contigency, and evaluates to F for p “ T and q “ T.

2. pp Ñ qq ˛ p␣q ^ pq. Options

• Tautology.
• Contradiction.
• Contigency, and evaluates to F for p “ F and q “ T.
• Contigency, and evaluates to F for p “ T and q “ F.
• Contigency, and evaluates to F for p “ T and q “ T.

3. pp ˛ qq Ñ q. Options

• Tautology.
• Contradiction.
• Contigency, and evaluates to F for p “ F and q “ F.
• Contigency, and evaluates to F for p “ F and q “ T.
• Contigency, and evaluates to F for p “ T and q “ T.

2 New Connective (2) (Supp)

Define the connective ˛ (same as the previous questions) via the following truth table:

p q p ˛ q

F F T

F T T

T F T

T T F

Show that the set t˛u is expressively complete.

3 Propositional logic+ND (Supp)

Determine, and explicitly mention, if the formula below is a tautology, contradiction, or contingency␣pp _ p␣p _ qqq.

• If tautology, give a proof in Natural Deduction. Use only the rules given in this appendix (14 and justify every step of your proof;

• If contradiction, give a proof in Natural Deduction of its negation (i.e. of the formula prefixed with a negation symbol). Use only the rules given in this appendix and justify every step of your proof;

• If contingency, give two truth-assignments to its variables, one that makes the formula false, and one that makes it true.

4 FOL+ND (Supp)

Show that the rule

Dx.@y.Ppx, yq

␣@x.Dy.␣Ppx, yq

is derivable in natural deduction.

Use only the rules given in this Appendix 14 and justify every step of your proof.

5 Structural Induction (Supp)

Consider the definition of binary trees in the lectures

data Tree a = Nul | Node (Tree a) a (Tree a)

and the following two functions:

sum :: Tree Int -> Int

sum Null = 0 — S1

sum Node l _ r = 1 + sum l + sum r — S2

and

treeCat :: Tree Int -> Tree Int -> Tree Int

treeCat Null t = t — TC1

treeCat (Node l x r) t = Node l x (treeCat r t) — TC2

The goal of this exercise is to show that for all t1,t2 of type Tree Int

sum (treeCat t1 t2) = sum t1 + sum t2.

Answer each of the following questions either in the textbox below, or by uploading a single jpg, png or pdf file that contains answers to all questions below.

1. What precisely should we prove by induction? State a property P, including possible quantifiers, so that proving @t.Pptq by induction implies the (above) goal of this exercise.

2. State (including possible quantifiers) and prove the base case goal.
3. State (including possible quantifiers) the inductive hypotheses of the proof.
4. State (including possible quantifiers) and prove the step case goal.

Solution:

1. Pptq “ @ t1 sum ptreeCat t t1q “ sumt ` sumt1.
2. Base case :

PpNullq “ @ t1 sum ptreeCat Null t1q “ sumNull ` sumt1.

Proof : for some tree t1

LHS “ sumptreeCat Null T1q

“ sumpt1q ´ ´ ´ T1

“ 0 ` sumpt1q ´ ´ ´ math

“ sumpNulq ` sumpt1q ´ ´S1

“ RHS

3. We assume that for arbitrary trees t1 and t2

Pplq “ @ t1 sum ptreeCat l t1q “ sumplq ` sumpt1q ´ ´ ´ IH1

Pprq “ @ t1 sum ptreeCat r t1q “ sumprq ` sumpt1q ´ ´ ´ IH2

4. T.P.T.

@x @t1 sum ptreeCat pNode l x rq t1q “ sumpNode l x rq ` sumt1 that is @x PpNode l x rq

Proof: for some x and t1 we prove the following

LHS “ sum ptreeCat pNode l x rq t1q

“ sum pl x ptreeCat r t1qq ´ ´ ´ T C2

“ 1 ` sumplq ` sumptreeCat r t1q ´ ´ ´ S2

“ 1 ` sumplq ` sumprq ` sumpt1q ´ ´ ´ IH2

“ sumpl x rq ` sumpt1q ´ ´ ´ S2

“ RHS

6 Hoare Logic (Supp+DA)

Consider the Hoare logic program

ty ą“ 1 ^ x “ 0u

while px 2 ă yq do

x :“ x ` 1

tpx ´ 1q 2 ď y ^ y ď x 2 u