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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
(* -------------------------------------------------------------------------------------------------------------------- *)
(* ----------------------------------- Data types useful for our theorem prover(s) ------------------------------------ *)
(* -------------------------------------------------------------------------------------------------------------------- *)
type proposition = (* logical proposition *)
| True
| False
| Lit of string
| Not of proposition
| And of proposition * proposition
| Or of proposition * proposition
| Implies of proposition * proposition
| Iff of proposition * proposition;;
type interpretation = (string * bool) list;; (* interpretation *)
type substitution = (string * proposition) list;; (* allows us to substitute any proposition for any atomic literal *)
(* -------------------------------------------------------------------------------------------------------------------- *)
(* ----------------------------------------- Utility functions for debugging ------------------------------------------ *)
(* -------------------------------------------------------------------------------------------------------------------- *)
let rec string_of_prop = function
| True -> "True"
| False -> "False"
| Lit symbol -> symbol
| Not p -> "¬" ^ (string_of_prop p)
| And (p1, p2) -> "(" ^ (string_of_prop p1) ^ " ∧ " ^ (string_of_prop p2) ^ ")"
| Or (p1, p2) -> "(" ^ (string_of_prop p1) ^ " ∨ " ^ (string_of_prop p2) ^ ")"
| Implies (p1, p2) -> "(" ^ (string_of_prop p1) ^ " → " ^ (string_of_prop p2) ^ ")"
| Iff (p1, p2) -> "(" ^ (string_of_prop p1) ^ " ↔ " ^ (string_of_prop p2) ^ ")";;
let string_of_sub sub =
let rec stringify = function
| [] -> ""
| (s, value) :: [] -> "(" ^ s ^ ": " ^ (string_of_prop value) ^ ")"
| (s, value) :: tl -> "(" ^ s ^ ": " ^ (string_of_prop value) ^ "), " ^ (stringify tl)
in "[" ^ (stringify sub) ^ "]";;
let string_of_interpr (i : interpretation) =
let rec stringify = function
| [] -> ""
| (s, value) :: [] -> "(" ^ s ^ ": " ^ (string_of_bool value) ^ ")"
| (s, value) :: tl -> "(" ^ s ^ ": " ^ (string_of_bool value) ^ "), " ^ (stringify tl)
in "[" ^ (stringify i) ^ "]";;
let print_prop prop = print_endline (string_of_prop prop);;
(* -------------------------------------------------------------------------------------------------------------------- *)
(* ------------------------------ Utility functions for dealing with our new data types ------------------------------- *)
(* -------------------------------------------------------------------------------------------------------------------- *)
(* Converts an interpretation to a substitution *)
let rec sub_of_interpr = function
| [] -> []
| (s, b) :: tl -> (s, if b then True else False) :: (sub_of_interpr tl);;
(* Removes instances of True or False literals via simplification *)
let rec simplify_true_false = function
| True -> True
| False -> False
| Lit symbol -> Lit symbol
| Not p ->
(match simplify_true_false p with
| True -> False
| False -> True
| Not p' -> p'
| p' -> Not(p'))
| And (p1, p2) ->
(match simplify_true_false p1, simplify_true_false p2 with
| False, _ -> False
| _, False -> False
| True, p2' -> p2'
| p1', True -> p1'
| p1', p2' -> And(p1', p2'))
| Or (p1, p2) ->
(match simplify_true_false p1, simplify_true_false p2 with
| True, _ -> True
| _, True -> True
| False, p2' -> p2'
| p1', False -> p1'
| p1', p2' -> Or(p1', p2'))
| Implies (p1, p2) ->
(match simplify_true_false p1, simplify_true_false p2 with
| False, _ -> True
| True, p2' -> p2'
| p1', p2' -> Implies(p1', p2'))
| Iff (p1, p2) ->
(match simplify_true_false p1, simplify_true_false p2 with
| True, p2' -> p2'
| p1', True -> p1'
| False, p2' -> simplify_true_false (Not(p2'))
| p1', False -> simplify_true_false (Not(p1'))
| p1', p2' -> Implies(p1', p2'));;
(* Finds a symbol in a list of substitutions and returns the value to substitute for that symbol *)
let rec replace sub symbol =
match sub with
| [] -> Lit symbol
| (s, value) :: sub -> if s = symbol then value else replace sub symbol;;
(* Substitutes propositions for symbols as specified by the sub argument *)
let rec substitute (prop : proposition) (sub : substitution) =
match prop with
| True -> True
| False -> False
| Lit s -> replace sub s
| Not p -> Not (substitute p sub)
| And(p1, p2) -> And(substitute p1 sub, substitute p2 sub)
| Or(p1, p2) -> Or(substitute p1 sub, substitute p2 sub)
| Implies(p1, p2) -> Implies(substitute p1 sub, substitute p2 sub)
| Iff(p1, p2) -> And(substitute p1 sub, substitute p2 sub);;
(* Converts a proposition to negation normal form *)
let to_nnf prop =
let rec to_nnf = function
| True -> True
| False -> False
| Lit symbol -> Lit symbol
| Not p ->
(match to_nnf p with
| And(p1, p2) -> Or(to_nnf (Not(p1)), to_nnf (Not(p2)))
| Or(p1, p2) -> And(to_nnf (Not(p1)), to_nnf (Not(p2)))
| p' -> simplify_true_false (Not p'))
| And(p1, p2) -> And(to_nnf p1, to_nnf p2)
| Or(p1, p2) -> Or(to_nnf p1, to_nnf p2)
| Implies(p1, p2) -> to_nnf (Or(Not(p1), p2))
| Iff(p1, p2) -> to_nnf (And(Implies(p1, p2), Implies(p2, p1)))
in
simplify_true_false (to_nnf prop);;
(* Applies an interpretation to a proposition and returns the resulting proposition *)
let interpret prop i = simplify_true_false (substitute prop (sub_of_interpr i));;
(* Tests whether a proposition holds under a given interpretation *)
let test_interpretation prop i =
match interpret prop i with
| True -> Some true
| False -> Some false
| _ -> None;; (* return None if cannot be determined *)
(* -------------------------------------------------------------------------------------------------------------------- *)
(* ------------------------------------------------------ Examples ---------------------------------------------------- *)
(* -------------------------------------------------------------------------------------------------------------------- *)
let show_example p i =
print_endline ("Proposition p: " ^ (string_of_prop p));
print_endline ("p in NNF: " ^ (string_of_prop (to_nnf p)));
print_endline ("Interpretation i: " ^ (string_of_interpr i));
print_endline ("p under i: " ^ (string_of_prop (interpret p i)) ^ "\n");;
let p1 = Not(Not(Not(And(Lit "a", Lit "b"))));;
let p2 = Iff(Not(Implies(Or(Lit "a", Lit "b"), And(Lit "b", Lit "c"))), True);;
let i1 = [("a", false); ("b", true); ("c", false)];;
let i2 = [("a", false); ("b", false)];;
let i3 = [("c", true)];;
show_example p1 i1;;
show_example p1 i2;;
show_example p1 i3;;
show_example p2 i1;;
show_example p2 i2;;
show_example p2 i3;;
|
