-
Notifications
You must be signed in to change notification settings - Fork 13
/
test-parents-2.limbo
71 lines (55 loc) · 3.18 KB
/
test-parents-2.limbo
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
Sort Human
Name Sally, Mia, Frank, Fred -> Human
Fun spouseOf/1, motherOf/1, fatherOf/1 -> Human
Var x, y, z -> Human
Rigid Sort Action
Fun bear/2 -> Action
Fun test/2 -> Action
Var a -> Action
Sort Result
Name Yes -> Result
Name No -> Result
Var r -> Result
Sensor Fun sf/Action -> Result
Real: spouseOf(Mia) = Frank
KB: spouseOf(Mia) = Frank v spouseOf(Mia) = Fred
KB: [] [a] motherOf(x) = y <-> a = bear(y,x) v a /= bear(y,x) ^ motherOf(x) = y
KB: [] [a] fatherOf(x) = y <-> ex z (a = bear(z,x) ^ spouseOf(z) = y) v fa z (a /= bear(z,x) ^ fatherOf(x) = y)
// KB: [] sf(a) = r <-> (ex x ex y (a = test(x,y) ^ fatherOf(x) = y) -> r = Yes) ^ (~ ex x ex y (a = test(x,y) ^ fatherOf(x) = y) -> r = No)
KB: [] sf(a) = r <-> ex x ex y (a = test(x,y) ^ fatherOf(x) = y ^ r = Yes) v fa x fa y (a /= test(x,y) v fatherOf(x) /= y) ^ r = No
// KB: [] sf(test(y,x)) = r <-> (fatherOf(x) = y -> r = Yes) ^ (fatherOf(x) /= y -> r = No)
// KB: [] sf(a) = r <-> r = r
Assert: spouseOf(Mia) = Frank
Assert: REG K<0> (spouseOf(Mia) = Frank v spouseOf(Mia) = Fred)
Refute: REG K<2> (motherOf(Sally) = Mia)
Refute: REG K<2> (fatherOf(Sally) = Frank v fatherOf(Sally) = Fred)
Refute: REG ex x K<2> (spouseOf(Mia) = x)
Assert: REG K<1> ex x (spouseOf(Mia) = x)
Assert: REG [bear(Mia,Sally)] K<0> (motherOf(Sally) = Mia)
Refute: REG [bear(Mia,Sally)] K<2> (motherOf(Sally) = Frank)
Refute: REG [bear(Mia,Sally)] K<2> (motherOf(Sally) = Fred)
Refute: REG [bear(Mia,Sally)] K<2> (spouseOf(Mia) = Frank)
Refute: REG [bear(Mia,Sally)] K<2> (spouseOf(Mia) = Fred)
Refute: REG [bear(Mia,Sally)] K<2> (fatherOf(Sally) = Frank)
Assert: REG [bear(Mia,Sally)] M<1> (fatherOf(Sally) /= Frank)
Assert: REG [bear(Mia,Sally)] M<2> (fatherOf(Sally) /= Frank)
Refute: REG [bear(Mia,Sally)] K<2> (fatherOf(Sally) = Fred)
Refute: REG [bear(Mia,Sally)] ex x K<2> (fatherOf(Sally) = x)
Assert: REG [bear(Mia,Sally)] K<1> ex x (fatherOf(Sally) = x)
Assert: REG K<1> [bear(Mia,Sally)] (fatherOf(Sally) = Frank v fatherOf(Sally) = Fred)
Refute: REG [bear(Mia,Sally)] K<0> (fatherOf(Sally) = Frank v fatherOf(Sally) = Fred)
Assert: REG [bear(Mia,Sally)] K<1> (fatherOf(Sally) = Frank v fatherOf(Sally) = Fred)
Refute: REG sf(test(Sally,Frank)) = Yes
Refute: REG sf(test(Sally,Frank)) = No
Assert: REG [bear(Mia,Sally)] sf(test(Sally,Frank)) = Yes
Refute: REG [bear(Mia,Sally)] sf(test(Sally,Frank)) = No
Refute: REG [bear(Mia,Sally)] [test(Sally,Frank)] K<0> fatherOf(Sally) = Frank
Assert: REG [bear(Mia,Sally)] [test(Sally,Frank)] K<1> fatherOf(Sally) = Frank
Refute: REG [bear(Mia,Sally)] [test(Sally,Frank)] K<0> fatherOf(Sally) /= Fred
Assert: REG [bear(Mia,Sally)] [test(Sally,Frank)] K<1> fatherOf(Sally) /= Fred
Assert: REG [bear(Mia,Sally)] [test(Sally,Frank)] M<1> fatherOf(Sally) /= Fred
Refute: REG [bear(Mia,Sally)] [test(Sally,Frank)] K<1> (fatherOf(Sally) = Frank ^ Yes /= Yes)
Refute: REG [bear(Mia,Sally)] [test(Sally,Fred)] K<0> fatherOf(Sally) = Frank
Assert: REG [bear(Mia,Sally)] [test(Sally,Fred)] K<1> fatherOf(Sally) = Frank
Refute: REG [bear(Mia,Sally)] [test(Sally,Fred)] K<0> fatherOf(Sally) /= Fred
Assert: REG [bear(Mia,Sally)] [test(Sally,Fred)] K<1> fatherOf(Sally) /= Fred