-
Notifications
You must be signed in to change notification settings - Fork 0
/
tests.jl
132 lines (119 loc) · 4.42 KB
/
tests.jl
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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
include("hw2.jl")
# ======================= Verifying Theory of Signature
println("$(repeat("=", 15)) KB & Signature Tests $(repeat("=", 15))")
sigma = Sigma(["John", "T"], [("g", 1), ("bar", 1)], [("Tree", 1), ("Taller", 2), ("Human", 1)])
println(sigma)
clauses = [["∀ t((Human(John) & Tree(t)) ==> ~Taller(John, t))",
"∀ x(∃ t(Human(x) ==> (Tree(y) & Taller(x, y))))"],
["∀ t((Human(John) & Tree(t)) ==> ~Taller(John, t))",
"∀ x(∃ t(Human(x) ==> (Tree(y) & Shorter(x, y))))"],
["∀ t((Human(John) & Tree(t)) ==> ~Taller(John, (f(t))))",
"∀ x(∃ t(Human(x) ==> (Tree(y) & Taller(x, y))))"],
["∀ t((Human(John) & Tree(t)) ==> ~Taller(John, C))",
"∀ x(∃ t(Human(x) ==> (Tree(y) & Taller(x, y))))"]]
explainations = ["All relations, functions, and constants in KB are in Sigma",
"KB contains a Relation that is NOT in Sigma",
"KB contains a Function that is NOT in Sigma",
"KB contains a Constant that is NOT in Sigma"]
for i=1:length(clauses)
println("($i)")
kb = KnowledgeBase(map(skolemize, map(toCNF, map(toClause, map(lexer, clauses[i])))))
println(kb)
try
verifyTheory(kb, sigma)
println(explainations[i])
catch
println("FAIL")
println(explainations[i])
end
println()
end
# ======================= Skolemization
println("$(repeat("=", 15)) Skolemization Tests $(repeat("=", 15))")
clauses = ["∃ x(∀ y(∀ z(∃ u (∀ v(∃ w(P(x,y,z,u,v,w)))))))",
"∀ x(∃ y(∃ z((~P(x, y) & Q(x, z)) | R(x, y, z))))",
"∀ x(∀ y(∃ z(∀ w(∃ u(P(x, y) & (Q(z,w) | R(u)))))))",
"∀ x(Philo(x) ==> ∃ y(Book(y) & Write(x, y)))",
"∀ x(∀ y((Philo(x) & StudentOf (y, x)) ==> ∃ z(Book(z) & Write(x, z) & Read(y, z))))",
"∃ x(∃ y(Philo(x) & StudentOf(y, x)))"]
for i=1:length(clauses)
println("($i)")
s = toCNF(toClause(lexer(clauses[i])))
print("\tStatement:\t");printCNF(s);println()
skolemized_s = skolemize(s)
print("\tSkolemized:\t");printCNF(skolemized_s);println("\n")
end
# ======================= CNF form
println("$(repeat("=", 15)) CNF Tests $(repeat("=", 15))")
clauses = ["∀ x(∀ y((Philo(x) & StudentOf (y, x)) ==> ∃ z(Book(z) & Write(x, z) & Read(y, z))))", "∀ x(Philo(x) ==> ∃ y(Book(y) & Write(x, y)))"]
for i=1:length(clauses)
println("($i)")
s = toClause(lexer(clauses[i]))
t = toCNF(toClause(lexer(clauses[i])))
print("\tStatement:\t");printCNF(s);println()
print("\tCNF:\t\t");printCNF(t);println("\n")
end
# It is incorporated in all other functions.
# ======================= Unification MGU
println("$(repeat("=", 15)) Unification Tests $(repeat("=", 15))")
clauses = [["P((f(x)))", "P((g(y)))"],
["P(x)", "P((f(y)))"],
["p((f(a)),(g(X)))", "p(Y,Y)"],
["P(A,x)", "P(B,x)"],
["P(A,x)", "P(A,y)"],
["P(x,(f(x)))", "P((f(x)),x)"]]
for i=1:length(clauses)
cnf = map(toCNF, map(toClause, map(lexer, clauses[i])))
print("Unify: ");printCNF(cnf[1]);print("\t");printCNF(cnf[2]);println()
println(cnf[2])
resolvants = MGU(cnf[1], cnf[2])
unifiers = nothing
if length(resolvants) == 2
unifiers, flip = resolvants
else
unifiers = resolvants
end
if unifiers == false || length(unifiers) == 0
print("Not Unifiable")
else
print("θs: ");print(printUnifiers(unifiers))
end
println("\n")
end
# ======================= Resolution
# (check Examples directory for bigger resolution problems)
println("$(repeat("=", 15)) Resolution Tests $(repeat("=", 15))")
println("(1)")
clauses = ["∀ x(I(x) ==> H(x))",
"~H(D)"]
query = "~I(D)"
cnf_clauses = map(skolemize, map(toCNF, map(toClause, map(lexer, clauses))))
kb = KnowledgeBase(cnf_clauses)
println(kb)
println("Does the KB entail $query?")
query = toClause(lexer(query))
resolve(kb, query)
println()
println("(2)")
clauses = ["∀ x(I(x) ==> H(x))",
"~H(D)"]
query = "H(x)"
cnf_clauses = map(skolemize, map(toCNF, map(toClause, map(lexer, clauses))))
kb = KnowledgeBase(cnf_clauses)
println(kb)
println("Does the KB entail $query?")
query = toClause(lexer(query))
resolve(kb, query)
println()
println("(3)")
clauses = ["Mother(Lulu, Fifi)", "Alive(Lulu)",
"∀ x(∀ y(Mother(x,y) ==> Parent(x,y)))",
"∀ x(∀ y((Parent(x,y) & Alive(x)) ==> Older(x,y)))"]
query = "Older(Lulu, Fifi)"
cnf_clauses = map(skolemize, map(toCNF, map(toClause, map(lexer, clauses))))
kb = KnowledgeBase(cnf_clauses)
println(kb)
println("Does the KB entail $query?")
query = toClause(lexer(query))
resolve(kb, query)
println()