1
2
3
4
5
6
7
8
9 """
10 A module to perform nonmonotonic reasoning
11 """
12
13 from nltk.sem.logic import *
14 from nltk.inference import inference
15 from nltk.inference.api import Prover
16 from nltk import defaultdict
17
19 """
20 A base decorator for the C{ProverCommand} class from which concrete
21 prover command decorators can extend.
22 """
24 """
25 @param proverCommand: C{ProverCommand} to decorate
26 """
27 self._proverCommand = proverCommand
28
29 - def prove(self, verbose=False):
33
36
39
42
45
46
47 -class ClosedDomainProver(ProverCommandDecorator):
48 """
49 This is a prover decorator that adds domain closure assumptions before
50 proving.
51 """
52 - def assumptions(self):
53 """
54 - Domain = union([e.free(False) for e in all_expressions])
55 - translate "exists x.P" to "(z=d1 | z=d2 | ... ) & P.replace(x,z)" OR
56 "P.replace(x, d1) | P.replace(x, d2) | ..."
57 - translate "all x.P" to "P.replace(x, d1) & P.replace(x, d2) & ..."
58 """
59 assumptions = [a for a in self._proverCommand.assumptions()]
60
61 domain = set()
62 for a in assumptions + [-self._proverCommand.goal()]:
63 domain |= (a.free(False) - a.free(True))
64
65 new_assumptions = set()
66 self._handle_quant_ex(self._proverCommand.goal(), domain, assumptions)
67 while assumptions:
68 a = assumptions.pop()
69 if isinstance(a, VariableBinderExpression):
70 self._handle_quant_ex(a, domain, assumptions)
71 else:
72 new_assumptions.add(a)
73
74 return list(new_assumptions)
75
77 return self._proverCommand.goal()
78
79 - def _handle_quant_ex(self, ex, domain, assumptions):
80 if isinstance(ex, ExistsExpression):
81 newterms = [ex.term.replace(ex.variable, VariableExpression(d))
82 for d in domain]
83 assumptions.append(reduce(Expression.__or__, newterms))
84 elif isinstance(ex, AllExpression):
85 for d in domain:
86 assumptions.append(ex.term.replace(ex.variable,
87 VariableExpression(d)))
88
90 """
91 This is a prover decorator that adds unique names assumptions before
92 proving.
93 """
128
130 return self._proverCommand.goal()
131
133 """
134 This is a prover decorator that completes predicates before proving.
135
136 If the premises don't logically entail "P(A)" then add "-P(A)"
137 all x.(P(x) -> (x=A)) is the completion of P
138
139 walk(Socrates)
140 Socrates != Bill
141 + all x.(walk(x) -> (x = Socrates))
142 ----------------
143 -walk(Bill)
144
145 see(Socrates, John)
146 see(John, Mary)
147 Socrates != John
148 John != Mary
149 + all x.all y.(see(x,y) -> ((x=Socrates & y=John) | (x=John & y=Mary)))
150 ----------------
151 -see(Socrates, Mary)
152
153 all x.(ostrich(x) -> bird(x))
154 bird(Tweety)
155 -ostrich(Sam)
156 Sam != Tweety
157 + all x.(bird(x) -> (ostrich(x) | x=Tweety))
158 -------------------
159 -bird(Sam)
160 """
162 assumptions = self._proverCommand.assumptions()
163
164 predicates = self._make_predicate_dict(assumptions)
165
166 assumptions2 = []
167 for p,predHolder in predicates.iteritems():
168 new_sig = self._make_unique_signature(predHolder)
169 new_sig_exs = [IndividualVariableExpression(v) for v in new_sig]
170
171 disjuncts = []
172 for sig in predHolder.signatures:
173 equality_exs = []
174 for v1,v2 in zip(new_sig_exs, sig):
175 equality_exs.append(EqualityExpression(v1,v2))
176 disjuncts.append(reduce(Expression.__and__, equality_exs))
177
178 for prop in predHolder.properties:
179
180 bindings = {}
181 for v1,v2 in zip(new_sig_exs, prop[0]):
182 bindings[v2] = v1
183 disjuncts.append(prop[1].substitute_bindings(bindings))
184
185
186 antecedent = self._make_antecedent(p, new_sig)
187 consequent = reduce(Expression.__or__, disjuncts)
188 accum = ImpExpression(antecedent, consequent)
189
190
191 for new_sig_var in new_sig[::-1]:
192 accum = AllExpression(new_sig_var, accum)
193 assumptions2.append(accum)
194
195 return assumptions + assumptions2
196
198 """
199 This method figures out how many arguments the predicate takes and
200 returns a tuple containing that number of unique variables.
201 """
202 return tuple([unique_variable()
203 for i in range(predHolder.signature_len)])
204
210
212 """
213 Create a dictionary of predicates from the assumptions.
214
215 @param assumptions: a C{list} of C{Expression}s
216 @return: C{dict} mapping C{VariableExpression}s to of C{PredHolder}s
217 """
218 predicates = defaultdict(PredHolder)
219 for a in assumptions:
220 self._map_predicates(a, predicates)
221 return predicates
222
224 if isinstance(expression, ApplicationExpression):
225 (func, args) = expression.uncurry()
226 if isinstance(func, VariableExpression):
227 predDict[func].append_sig(tuple(args))
228 elif isinstance(expression, AndExpression):
229 self._map_predicates(expression.first, predDict)
230 self._map_predicates(expression.second, predDict)
231 elif isinstance(expression, AllExpression):
232
233 sig = [expression.variable]
234 term = expression.term
235 while isinstance(term, AllExpression):
236 sig.append(term.variable)
237 term = term.term
238 if isinstance(term, ImpExpression):
239 if isinstance(term.second, ApplicationExpression):
240 func = term.second.function
241 if isinstance(func, VariableExpression):
242 predDict[func].append_prop((tuple(sig), term.first))
243
245 return self._proverCommand.goal()
246
247
249 """
250 This class will be used by a dictionary that will store information
251 about predicates to be used by the C{ClosedWorldProver}.
252
253 The 'signatures' property is a list of tuples defining signatures for
254 which the predicate is true. For instance, 'see(john, mary)' would be
255 result in the signature '(john,mary)' for 'see'.
256
257 The second element of the pair is a list of pairs such that the first
258 element of the pair is a tuple of variables and the second element is an
259 expression of those variables that makes the predicate true. For instance,
260 'all x.all y.(see(x,y) -> know(x,y))' would result in "((x,y),('see(x,y)'))"
261 for 'know'.
262 """
264 self.signatures = []
265 self.properties = []
266 self.signature_len = None
267
271
275
277 if self.signature_len is None:
278 self.signature_len = len(new_sig)
279 elif self.signature_len != len(new_sig):
280 raise Exception("Signature lengths do not match")
281
283 return '(%s,%s,%s)' % (self.signatures, self.properties,
284 self.signature_len)
285
288
290 lp = LogicParser()
291
292 p1 = lp.parse(r'exists x.walk(x)')
293 p2 = lp.parse(r'man(Socrates)')
294 c = lp.parse(r'walk(Socrates)')
295 prover = inference.get_prover(c, [p1,p2])
296 print prover.prove()
297 cdp = ClosedDomainProver(prover)
298 for a in cdp.assumptions(): print a
299 print cdp.prove()
300
301 p1 = lp.parse(r'exists x.walk(x)')
302 p2 = lp.parse(r'man(Socrates)')
303 p3 = lp.parse(r'-walk(Bill)')
304 c = lp.parse(r'walk(Socrates)')
305 prover = inference.get_prover(c, [p1,p2,p3])
306 print prover.prove()
307 cdp = ClosedDomainProver(prover)
308 for a in cdp.assumptions(): print a
309 print cdp.prove()
310
332
334 lp = LogicParser()
335
336 p1 = lp.parse(r'walk(Socrates)')
337 p2 = lp.parse(r'(Socrates != Bill)')
338 c = lp.parse(r'-walk(Bill)')
339 prover = inference.get_prover(c, [p1,p2])
340 print prover.prove()
341 cwp = ClosedWorldProver(prover)
342 for a in cwp.assumptions(): print a
343 print cwp.prove()
344
345 p1 = lp.parse(r'see(Socrates, John)')
346 p2 = lp.parse(r'see(John, Mary)')
347 p3 = lp.parse(r'(Socrates != John)')
348 p4 = lp.parse(r'(John != Mary)')
349 c = lp.parse(r'-see(Socrates, Mary)')
350 prover = inference.get_prover(c, [p1,p2,p3,p4])
351 print prover.prove()
352 cwp = ClosedWorldProver(prover)
353 for a in cwp.assumptions(): print a
354 print cwp.prove()
355
356 p1 = lp.parse(r'all x.(ostrich(x) -> bird(x))')
357 p2 = lp.parse(r'bird(Tweety)')
358 p3 = lp.parse(r'-ostrich(Sam)')
359 p4 = lp.parse(r'Sam != Tweety')
360 c = lp.parse(r'-bird(Sam)')
361 prover = inference.get_prover(c, [p1,p2,p3,p4])
362 print prover.prove()
363 cwp = ClosedWorldProver(prover)
364 for a in cwp.assumptions(): print a
365 print cwp.prove()
366
380
381 if __name__ == '__main__':
382 closed_domain_demo()
383 unique_names_demo()
384 closed_world_demo()
385 combination_prover_demo()
386