Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

**Solutions for exams**

Can we expect the missing solutions for some exams to be published before our exam?

Espacially the proofs are a little frustrating, because there are already not to many tasks avaible to practice…

Solutions missing:

WS1617 3.3

WS1617 retake 4.1 & 4.3

WS1718 5.2

WS19/20 4

Realistically, that’s going to be difficult.

I’ll have a look by Friday but am not promising.

Here is what i have. No warranty! Feel free to correct

WS1617 3.3

V = {vi | i ∈ {1, …, 50}}

∀v∈V: D = Dv = {1, …, 50}

∀ui,uj∈V: C_ui,uj = C_uj,ui = {(di, dj) ∈ D x D | di = dj} for: di ≠ dj ∧ |i-j| ≠ |di-dj|

WS1617 retake 4.1

1 (A∧B∧C)⇒(A ⇒ B∧C)^F

2 (A∧B∧C)^T

3 (A⇒B∧C)^F

4 A^T

5 B^T

6 C^T

7 A^T

8 B∧C^F

9 B^F | C^F

10 ⊥ | ⊥

WS1617 retake 4.3 (looks terrible)

1 (X∧Y)∨(X∧¬Y)⇒Xf

2 (X∧Y)∨(X∧¬Y)t ; Xf

3 (X∧Y)t ∨(X∧¬Y)t ; Xf

4 Xt∨(X∧¬Y)t ; Yt∨(X∧¬Y)t ; Xf

5 Xt∨Xt ; Xt∨¬Yt ; Yt∨Xt ; Yt∨¬Yt ; Xf

6 Xt ; Xt∨Yt ; Yt∨Xt ; Yt∨Yf ; Xf

clauses: {Xt} {Xt, Yf} {Yt, Xt} {Yt, Yf} {Xf}

{Xt} + {Xf} → {}

WS17/18 5.2 (looks even more terrible)

1 ∃X((∃Y¬P(Y, f(b))) ∨ ¬(P(b, f(X)) ⇒ ¬P(g(a), f(X)))^F

2 ((∃Y¬P(Y, f(b))) ∨ ¬(P(b, f(V)) ⇒ ¬P(g(a), f(V)))^F

3 (∃Y¬P(Y, f(b))^F

4 ¬(P(b, f(V)) ⇒ ¬P(g(a), f(V)))^F

5 P(b, f(V)) ⇒ ¬P(g(a), f(V))^T

6 ¬P(W, f(b))^F

7 P(W, f(b))^T

8 P(b, f(V))^F | ¬P(g(a), f(V)))^T

9 ⊥:[b/W],[b/V] | P(g(a), f(V)))^F

10 | (not closable!)

WS19/20 4

- q2={1}, q3={2, 4}, q4={1,2,4}
- A variable u is arc-consistent relative to another variable v if either there are no constraints between u and v or ∀d ∈ Du there is at least one d’ ∈ Dv

such that (d, d’) ∈ C.

AfterQ2→Q1: q2={1}, q3={1, 2, 3, 4}, q4={1, 2, 3, 4}

AfterQ3→Q1: q2={1}, q3={2, 4}, q4={1, 2, 3, 4}

AfterQ2→Q3: q2={1}, q3={2, 4}, q4={1, 2, 3, 4}

AfterQ3→Q2: q2={1}, q3={4}, q4={1, 2, 3, 4}

4. When the whole constraint network is arc-consistent

Thank you very much Bsanchez for your solutions! I got the same results as you except for in WS 17/18 5.2.

The Tableaux should be closable, you could apply the ∃^F (3-6) again in the right branch and get yourself a ¬P(Z,f(b))^F for example ( I marked my changes red):

…

7 P(W, f(b))^T

8 P(b, f(V))^F | ¬P(g(a), f(b)))^T

9 ⊥:[b/W],[b/V] | P(g(a), f(b)))^F

10 | ¬ P(Z, f(b)) ^F (from line 3)

11 | P(Z, f(b)) ^T

12 | ⊥:[g(a)/ Z]

It is explained in this video nugget: https://www.fau.tv/clip/id/26912

Hello matze123, no problem i hoped actually that someone would correct me on this problem. So thank you too!

I mixed up the multiplicity characteristics with existsT and existsF. Your correction looks good to me.

EDIT:

maybe line 10 should be turned in P(Z, f(b))^T first, but that’s just a small thing …

Its always best to debate about solutions, that’s what’s really missing in the whole online semester… You’re right about the last step, I corrected it.

WS19/20 4

- … shouldn’t Q4={2,4}, since Q2 is already assigned by 1?

nevermind! the only assignment happening (in terms of forward checking) is Q1 ← 3 (I guess)

correct, that’s why arc-consistency subsumes forward checking