1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:
19:
20:
21:

from z3 import EnumSort, Consts, Distinct, Implies, And, Or, Solver, sat

preds = ("der Junge", "das Maedchen", "die Katze", "der Hund")
roles, (J, M, K, H) = EnumSort('roles', preds)
(a, b, c, d) = Consts('a b c d', roles)
names = ("Aki", "Bauzi", "Knirps", "Dicki")

s = Solver()
s.add([
    Implies(And(a != J, b != M), c == H),
    Implies(d != K, Implies(a != M, b == H)),
    Or(c == K, d == J, a == H),
    Implies(And(c != M, d != M), b == H),
    Distinct(a, b, c, d)
])

while s.check() == sat:
    m = s.model()
    for (name, x) in zip(names, [a, b, c, d]):
        print(f"{name} ist {m[x]}.")
    s.add(Or(a != m[a], b != m[b], c != m[c], d != m[d]))

1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:

from itertools import permutations

implies = lambda A, B: not A or B
X = ("Aki", "Bauzi", "Knirps", "Dicki")
(a, b, c, d) = X
for (J, M, K, H) in permutations(X):
    if (implies(a!=J and b!=M, c==H) and
        implies(d!=K, implies(a!=M, b==H)) and
        (c==K or d==J or a==H) and
        implies(c!=M and d!=M, b==H)):
        print(f"Junge: {J}.\nMädchen: {M}.\nKatze: {K}.\nHund: {H}.")

1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:
19:
20:
21:
22:
23:
24:
25:
26:
27:
28:
29:
30:
31:
32:
33:
34:
35:
36:
37:
38:
39:
40:
41:
42:
43:
44:
45:
46:
47:
48:
49:
50:
51:
52:
53:
54:
55:
56:
57:
58:
59:
60:
61:
62:
63:
64:
65:
66:
67:
68:
69:
70:
71:
72:
73:
74:
75:
76:
77:
78:
79:
80:

(* Definition der 4 Entitäten als induktiver Typ *)
Inductive Entity: Type := a | b | c | d.

Section Puzzle.

Variables J M K H: Entity.

(* Alle 4 Variablen sind paarweise verschieden (Permutation) *)
Hypothesis dist_JM: J <> M.
Hypothesis dist_JK: J <> K.
Hypothesis dist_JH: J <> H.
Hypothesis dist_MK: M <> K.
Hypothesis dist_MH: M <> H.
Hypothesis dist_KH: K <> H.

(* Die 4 Bedingungen aus dem Python-Code *)
Hypothesis cond1: J <> a /\ M <> b -> H = c.
Hypothesis cond2: K <> d -> M <> a -> H = b.
Hypothesis cond3: K = c \/ J = d \/ H = a.
Hypothesis cond4: M <> c /\ M <> d -> H = b.

(* Zwei triviale Hilfslemmata für den Beweisfluss *)
Lemma entity_cases (x: Entity): x = a \/ x = b \/ x = c \/ x = d.
Proof. destruct x; auto. Qed.

Lemma eq_dec (x y: Entity): x = y \/ x <> y.
Proof. decide equality. Qed.

(* Schritt 1: Beweis, dass H = b, per Widerspruch *)
Lemma H_is_b: H = b.
Proof.
  destruct (eq_dec H b) as [Hb | Hnb]; [exact Hb |].
  
  (* Wenn H <> b, folgt M <> a und M <> b aus cond4 *)
  assert (M_not_a: M <> a) by
    (intro; apply Hnb, cond4; split; congruence).
  assert (M_not_b: M <> b) by
    (intro; apply Hnb, cond4; split; congruence).
  
  (* Aus cond2 folgt dann zwingend K = d *)
  assert (K_is_d: K = d). {
    destruct (eq_dec K d); [assumption |].
    assert (H = b) by (apply cond2; assumption).
    congruence.
  }
  
  (* Aus cond3 folgt dann zwingend H = a *)
  assert (H_is_a: H = a) by (destruct cond3 as [|[|]]; congruence).
  
  (* Für M und J bleiben nur c und b *)
  assert (M_is_c: M = c) by
    (destruct (entity_cases M) as [|[|[|]]]; congruence).
  assert (J_is_b: J = b) by
    (destruct (entity_cases J) as [|[|[|]]]; congruence).
  
  (* Das führt durch cond1 zum Widerspruch *)
  assert (Hc : H = c) by (apply cond1; split; congruence).
  
  (* congruence erkennt, dass H=a und H=c nicht *)
  (* gleichzeitig gelten können *)
  congruence.
Qed.

(* Schritt 2: Der restliche Beweis schließt das Puzzle ab *)
Theorem solve_puzzle: J = a /\ M = d /\ K = c /\ H = b.
Proof.
  assert (Hb: H = b) by apply H_is_b.
  assert (Ja: J = a). {
    destruct (eq_dec J a); [assumption |].
    assert (H = c) by (apply cond1; split; congruence).
    congruence.
  }
  assert (Kc: K = c) by (destruct cond3 as [|[|]]; congruence).
  assert (Md: M = d) by
    (destruct (entity_cases M) as
      [|[|[|]]]; congruence).
  auto.
Qed.

End Puzzle.

1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:
19:
20:
21:
22:
23:
24:
25:
26:
27:
28:
29:
30:
31:
32:
33:
34:
35:
36:
37:
38:
39:
40:
41:
42:
43:
44:
45:
46:
47:
48:
49:
50:
51:
52:
53:
54:
55:
56:
57:
58:
59:

from math import gcd, lcm, prod
from itertools import islice, count, permutations

def is_prime(n):
    if n < 2: return False
    k = 2
    while k*k <= n:
        if n%k == 0: return False
        k += 1
    return True

(a, b, c, d) = (0, 1, 2, 3)
perms = list(permutations("JMKH"))
model_count = len(perms)

prime_iterator = (n for n in count(2) if is_prime(n))
prime_list = list(islice(prime_iterator, model_count))

BOTTOM = 1
TOP = prod(prime_list)
AND = lambda x, y: gcd(x, y)
OR = lambda x, y: lcm(x, y)
NOT = lambda x: TOP//x
IMPLIES = lambda x, y: OR(NOT(x), y)

# Superpostion der Modelle, die P(x) erfüllen.
def sp(P, x):
    acc = 1
    for (index, perm) in enumerate(perms):
        if perm[x] == P:
            acc *= prime_list[index]
    return acc

Ja = sp("J", a); Jd = sp("J", d)
Ma = sp("M", a); Mb = sp("M", b)
Mc = sp("M", c); Md = sp("M", d)
Ha = sp("H", a); Hb = sp("H", b)
Hc = sp("H", c); Hd = sp("H", d)
Kc = sp("K", c); Kd = sp("K", d)

C1 = IMPLIES(AND(NOT(Ja), NOT(Mb)), Hc)
C2 = IMPLIES(NOT(Kd), IMPLIES(NOT(Ma), Hb))
C3 = OR(OR(Kc, Jd), Ha)
C4 = IMPLIES(AND(NOT(Mc), NOT(Md)), Hb)

S = AND(AND(AND(C1, C2), C3), C4)
index = prime_list.index(S)
perm = perms[index]

display = {
    "J": "der Junge",
    "M": "das Mädchen",
    "K": "die Katze",
    "H": "der Hund"
}
names = ("Aki", "Bauzi", "Knirps", "Dicki")

for (name, x) in zip(names, (a, b, c, d)):
    print(f"{name} ist {display[perm[x]]}.")