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
|
%%% Name/LOGIN-ID Camil Staps / s4498062
%%% ACKNOWLEDGMENTS:
th_C: THEORY
%%%
%%% Prove using only (SPLIT), (FLATTEN), (INST), (SKOLEM), (LEMMA), (ASSERT)
%%% ~~~~
BEGIN
%%%
%%% Andy, Bob, Cindy, Dinah, Eve, Fred, and Gary live in the seven houses,
%%% numbered 1 through 7, on Maple Steet. Gary's address is 5 greater than
%%% Bob's. Bob's address is greater than Andy's. Dinah's address is
%%% less than Eve's, whose address is 2 less than Gary's. Cindy's address
%%% is less than either Dinah's or Fred's. Who lives where?
%%%
people: TYPE = {A, B, C, D, E, F, G}
address: [people -> int]
p,q: VAR people
%%%
%%% The axiom below asserts that each person's address is between 1 and 7.
%%%
Range: AXIOM address(p) = 1
or address(p) = 2
or address(p) = 3
or address(p) = 4
or address(p) = 5
or address(p) = 6
or address(p) = 7
%%%
%%% The axiom below states that each person's address is unique
%%%
Unique: AXIOM address(p) = address(q) implies p = q
%%%
%%% AXIOMs "clue1" through "clue7" translate the problem.
%%% The lemmas, together, give a solution. Each lemma
%%% is introduced as it becomes provable.
%%%
clue1: AXIOM address(B) + 5 = address(G)
L1: LEMMA address(B) = 1 or address(B) = 2
clue2: AXIOM address(B) > address(A)
L2: LEMMA address(B) = 2
L3: LEMMA address(A) = 1
L4: LEMMA address(G) = 7
clue3: AXIOM address(D) < address(E)
clue4: AXIOM address(E) + 2 = address(G)
L5: LEMMA address(E) = 5
L6: LEMMA address(D) = 3 or address(D) = 4
clue5: AXIOM address(C) < address(D)
L7: LEMMA address(C) = 3 and address(D) = 4
clue7: AXIOM address(C) < address(F)
L8: LEMMA address(F) = 6
END th_C
|
