nltk.inference.tableau

1 # Natural Language Toolkit: First-order Tableau-based Theorem Prover 2 # 3 # Author: Dan Garrette <[email protected]> 4 # 5 # URL: <http://nltk.org> 6 # For license information, see LICENSE.TXT 7 8 from nltk.sem.logic import * 9 10 from api import Prover, ProverCommand 11 12 """ 13 Module for a tableau-based First Order theorem prover. 14 """ 15

16 -class ProverParseError(Exception): pass

17

18 -class Tableau(Prover):

19 _assume_false=False 20

21 - def prove(self, goal=None, assumptions=[], debug=False):

22 result = None 23 try: 24 agenda = Agenda() 25 if goal: 26 agenda.put(-goal) 27 agenda.put_all(assumptions) 28 result = _attempt_proof(agenda, set(), set(), (debug, 0)) 29 except RuntimeError, e: 30 if self._assume_false and str(e).startswith('maximum recursion depth exceeded'): 31 result = False 32 else: 33 if debug: 34 print e 35 else: 36 raise e 37 return (result, '')

38

39 -class Agenda(object):

40 - def __init__(self):

41 self.sets = tuple(set() for i in range(17))

42

43 - def clone(self):

44 new_agenda = Agenda() 45 set_list = [s.copy() for s in self.sets] 46 47 new_allExs = set() 48 for allEx in set_list[Categories.ALL]: 49 new_allEx = AllExpression(allEx.variable, allEx.term) 50 try: 51 new_allEx._used_vars = set(used for used in allEx._used_vars) 52 except AttributeError: 53 new_allEx._used_vars = set() 54 new_allExs.add(new_allEx) 55 set_list[Categories.ALL] = new_allExs 56 57 set_list[Categories.N_EQ] = set(NegatedExpression(n_eq.term) 58 for n_eq in set_list[Categories.N_EQ]) 59 60 new_agenda.sets = tuple(set_list) 61 return new_agenda

62

63 - def __getitem__(self, index):

64 return self.sets[index]

65

66 - def put(self, expression):

67 if isinstance(expression, AllExpression): 68 ex_to_add = AllExpression(expression.variable, expression.term) 69 try: 70 ex_to_add._used_vars = set(used for used in expression._used_vars) 71 except AttributeError: 72 ex_to_add._used_vars = set() 73 else: 74 ex_to_add = expression 75 self.sets[self._categorize_expression(ex_to_add)].add(ex_to_add)

76

77 - def put_all(self, expressions):

78 for expression in expressions: 79 self.put(expression)

80

81 - def put_atoms(self, atoms):

82 for atom in atoms: 83 if atom[1]: 84 self[Categories.N_ATOM].add(-atom[0]) 85 else: 86 self[Categories.ATOM].add(atom[0])

87

88 - def pop_first(self):

89 """ Pop the first expression that appears in the agenda """ 90 for i in range(len(self.sets)): 91 if self.sets[i]: 92 if i in [Categories.N_EQ, Categories.ALL]: 93 for ex in self.sets[i]: 94 try: 95 if not ex._exhausted: 96 self.sets[i].remove(ex) 97 return(ex, i) 98 except AttributeError: 99 self.sets[i].remove(ex) 100 return(ex, i) 101 else: 102 return (self.sets[i].pop(), i) 103 return (None, None)

104 105

106 - def replace_all(self, old, new):

107 self.sets = tuple(set(ex.replace(old.variable, new) for ex in s) for s in self.sets)

108

109 - def mark_alls_fresh(self):

110 for u in self.sets[Categories.ALL]: 111 u._exhausted = False

112

113 - def mark_neqs_fresh(self):

114 for neq in self.sets[Categories.N_EQ]: 115 neq._exhausted = False

116

117 - def _categorize_expression(self, current):

118 if isinstance(current, AllExpression): 119 return Categories.ALL 120 elif isinstance(current, AndExpression): 121 return Categories.AND 122 elif isinstance(current, OrExpression): 123 return Categories.OR 124 elif isinstance(current, ImpExpression): 125 return Categories.IMP 126 elif isinstance(current, IffExpression): 127 return Categories.IFF 128 elif isinstance(current, EqualityExpression): 129 return Categories.EQ 130 elif isinstance(current, NegatedExpression): 131 return self._categorize_NegatedExpression(current) 132 elif isinstance(current, ExistsExpression): 133 return Categories.EXISTS 134 elif isinstance(current, ApplicationExpression): 135 return Categories.ATOM 136 else: 137 raise ProverParseError()

138

139 - def _categorize_NegatedExpression(self, current):

140 negated = current.term 141 142 if isinstance(negated, AllExpression): 143 return Categories.N_ALL 144 elif isinstance(negated, AndExpression): 145 return Categories.N_AND 146 elif isinstance(negated, OrExpression): 147 return Categories.N_OR 148 elif isinstance(negated, ImpExpression): 149 return Categories.N_IMP 150 elif isinstance(negated, IffExpression): 151 return Categories.N_IFF 152 elif isinstance(negated, EqualityExpression): 153 return Categories.N_EQ 154 elif isinstance(negated, NegatedExpression): 155 return Categories.D_NEG 156 elif isinstance(negated, ExistsExpression): 157 return Categories.N_EXISTS 158 elif isinstance(negated, ApplicationExpression): 159 return Categories.N_ATOM 160 else: 161 raise ProverParseError()

162

163 -def _attempt_proof(agenda, accessible_vars, atoms, debug=(False, 0)):

164 (current, category) = agenda.pop_first() 165 166 #if there's nothing left in the agenda, and we haven't closed the path 167 if not current: 168 debug_line('AGENDA EMPTY', (debug[0], debug[1]+1)) 169 return False 170 171 proof_method = { Categories.ATOM: _attempt_proof_atom, 172 Categories.N_ATOM: _attempt_proof_n_atom, 173 Categories.N_EQ: _attempt_proof_n_eq, 174 Categories.D_NEG: _attempt_proof_d_neg, 175 Categories.N_ALL: _attempt_proof_n_all, 176 Categories.N_EXISTS: _attempt_proof_n_some, 177 Categories.AND: _attempt_proof_and, 178 Categories.N_OR: _attempt_proof_n_or, 179 Categories.N_IMP: _attempt_proof_n_imp, 180 Categories.OR: _attempt_proof_or, 181 Categories.IMP: _attempt_proof_imp, 182 Categories.N_AND: _attempt_proof_n_and, 183 Categories.IFF: _attempt_proof_iff, 184 Categories.N_IFF: _attempt_proof_n_iff, 185 Categories.EQ: _attempt_proof_eq, 186 Categories.EXISTS: _attempt_proof_some, 187 Categories.ALL: _attempt_proof_all, 188 }[category] 189 190 debug_line(current, debug) 191 return proof_method(current, agenda, accessible_vars, atoms, debug)

192

193 -def debug_line(data, debug):

194 if debug[0]: 195 additional = '' 196 if isinstance(data, AllExpression): 197 try: 198 additional += ': %s' % str([ve.variable.name for ve in data._used_vars]) 199 except AttributeError: 200 additional += ': []' 201 202 if isinstance(data, Expression): 203 data = data 204 205 print '%s%s%s' % (' '*debug[1], data, additional)

206

207 -def _attempt_proof_atom(current, agenda, accessible_vars, atoms, debug=(False, 0)):

208 # Check if the branch is closed. Return 'True' if it is 209 if (current, True) in atoms: 210 debug_line('CLOSED', (debug[0], debug[1]+1)) 211 return True 212 213 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars 214 agenda.mark_alls_fresh(); 215 args = current.uncurry()[1] 216 return _attempt_proof(agenda, accessible_vars|set(args), atoms|set([(current, False)]), (debug[0], debug[1]+1))

217

218 -def _attempt_proof_n_atom(current, agenda, accessible_vars, atoms, debug=(False, 0)):

219 # Check if the branch is closed. Return 'True' if it is 220 if (current.term, False) in atoms: 221 debug_line('CLOSED', (debug[0], debug[1]+1)) 222 return True 223 224 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars 225 agenda.mark_alls_fresh(); 226 args = current.term.uncurry()[1] 227 return _attempt_proof(agenda, accessible_vars|set(args), atoms|set([(current.term, True)]), (debug[0], debug[1]+1))

228

229 -def _attempt_proof_n_eq(current, agenda, accessible_vars, atoms, debug=(False, 0)):

230 ########################################################################### 231 # Since 'current' is of type '~(a=b)', the path is closed if 'a' == 'b' 232 ########################################################################### 233 if current.term.first == current.term.second: 234 debug_line('CLOSED', (debug[0], debug[1]+1)) 235 return True 236 237 agenda[Categories.N_EQ].add(current) 238 current._exhausted = True 239 return _attempt_proof(agenda, accessible_vars|set([current.term.first, current.term.second]), atoms, (debug[0], debug[1]+1))

240

241 -def _attempt_proof_d_neg(current, agenda, accessible_vars, atoms, debug=(False, 0)):

242 agenda.put(current.term.term) 243 return _attempt_proof(agenda, accessible_vars, atoms, (debug[0], debug[1]+1))

244

245 -def _attempt_proof_n_all(current, agenda, accessible_vars, atoms, debug=(False, 0)):

246 agenda[Categories.EXISTS].add(ExistsExpression(current.term.variable, -current.term.term)) 247 return _attempt_proof(agenda, accessible_vars, atoms, (debug[0], debug[1]+1))

248

249 -def _attempt_proof_n_some(current, agenda, accessible_vars, atoms, debug=(False, 0)):

250 agenda[Categories.ALL].add(AllExpression(current.term.variable, -current.term.term)) 251 return _attempt_proof(agenda, accessible_vars, atoms, (debug[0], debug[1]+1))

252

253 -def _attempt_proof_and(current, agenda, accessible_vars, atoms, debug=(False, 0)):

254 agenda.put(current.first) 255 agenda.put(current.second) 256 return _attempt_proof(agenda, accessible_vars, atoms, (debug[0], debug[1]+1))

257

258 -def _attempt_proof_n_or(current, agenda, accessible_vars, atoms, debug=(False, 0)):

259 agenda.put(-current.term.first) 260 agenda.put(-current.term.second) 261 return _attempt_proof(agenda, accessible_vars, atoms, (debug[0], debug[1]+1))

262

263 -def _attempt_proof_n_imp(current, agenda, accessible_vars, atoms, debug=(False, 0)):

264 agenda.put(current.term.first) 265 agenda.put(-current.term.second) 266 return _attempt_proof(agenda, accessible_vars, atoms, (debug[0], debug[1]+1))

267

268 -def _attempt_proof_or(current, agenda, accessible_vars, atoms, debug=(False, 0)):

269 new_agenda = agenda.clone() 270 agenda.put(current.first) 271 new_agenda.put(current.second) 272 return _attempt_proof(agenda, accessible_vars, atoms, (debug[0], debug[1]+1)) and \ 273 _attempt_proof(new_agenda, accessible_vars, atoms, (debug[0], debug[1]+1))

274

275 -def _attempt_proof_imp(current, agenda, accessible_vars, atoms, debug=(False, 0)):

276 new_agenda = agenda.clone() 277 agenda.put(-current.first) 278 new_agenda.put(current.second) 279 return _attempt_proof(agenda, accessible_vars, atoms, (debug[0], debug[1]+1)) and \ 280 _attempt_proof(new_agenda, accessible_vars, atoms, (debug[0], debug[1]+1))

281

282 -def _attempt_proof_n_and(current, agenda, accessible_vars, atoms, debug=(False, 0)):

283 new_agenda = agenda.clone() 284 agenda.put(-current.term.first) 285 new_agenda.put(-current.term.second) 286 return _attempt_proof(agenda, accessible_vars, atoms, (debug[0], debug[1]+1)) and \ 287 _attempt_proof(new_agenda, accessible_vars, atoms, (debug[0], debug[1]+1))

288

289 -def _attempt_proof_iff(current, agenda, accessible_vars, atoms, debug=(False, 0)):

290 new_agenda = agenda.clone() 291 agenda.put(current.first) 292 agenda.put(current.second) 293 new_agenda.put(-current.first) 294 new_agenda.put(-current.second) 295 return _attempt_proof(agenda, accessible_vars, atoms, (debug[0], debug[1]+1)) and \ 296 _attempt_proof(new_agenda, accessible_vars, atoms, (debug[0], debug[1]+1))

297

298 -def _attempt_proof_n_iff(current, agenda, accessible_vars, atoms, debug=(False, 0)):

299 new_agenda = agenda.clone() 300 agenda.put(current.term.first) 301 agenda.put(-current.term.second) 302 new_agenda.put(-current.term.first) 303 new_agenda.put(current.term.second) 304 return _attempt_proof(agenda, accessible_vars, atoms, (debug[0], debug[1]+1)) and \ 305 _attempt_proof(new_agenda, accessible_vars, atoms, (debug[0], debug[1]+1))

306

307 -def _attempt_proof_eq(current, agenda, accessible_vars, atoms, debug=(False, 0)):

308 ######################################################################### 309 # Since 'current' is of the form '(a = b)', replace ALL free instances 310 # of 'a' with 'b' 311 ######################################################################### 312 agenda.put_atoms(atoms) 313 agenda.replace_all(current.first, current.second) 314 accessible_vars.discard(current.first) 315 agenda.mark_neqs_fresh(); 316 return _attempt_proof(agenda, accessible_vars, set(), (debug[0], debug[1]+1))

317

318 -def _attempt_proof_some(current, agenda, accessible_vars, atoms, debug=(False, 0)):

319 new_unique_variable = IndividualVariableExpression(unique_variable()) 320 agenda.put(current.term.replace(current.variable, new_unique_variable)) 321 agenda.mark_alls_fresh() 322 return _attempt_proof(agenda, accessible_vars|set([new_unique_variable]), atoms, (debug[0], debug[1]+1))

323

324 -def _attempt_proof_all(current, agenda, accessible_vars, atoms, debug=(False, 0)):

325 try: 326 current._used_vars 327 except AttributeError: 328 current._used_vars = set() 329 330 #if there are accessible_vars on the path 331 if accessible_vars: 332 # get the set of bound variables that have not be used by this AllExpression 333 bv_available = accessible_vars - current._used_vars 334 335 if bv_available: 336 variable_to_use = list(bv_available)[0] 337 debug_line('--> Using \'%s\'' % variable_to_use, (debug[0], debug[1]+2)) 338 current._used_vars |= set([variable_to_use]) 339 agenda.put(current.term.replace(current.variable, variable_to_use)) 340 agenda[Categories.ALL].add(current) 341 return _attempt_proof(agenda, accessible_vars, atoms, (debug[0], debug[1]+1)) 342 343 else: 344 #no more available variables to substitute 345 debug_line('--> Variables Exhausted', (debug[0], debug[1]+2)) 346 current._exhausted = True 347 agenda[Categories.ALL].add(current) 348 return _attempt_proof(agenda, accessible_vars, atoms, (debug[0], debug[1]+1)) 349 350 else: 351 new_unique_variable = IndividualVariableExpression(unique_variable()) 352 debug_line('--> Using \'%s\'' % new_unique_variable, (debug[0], debug[1]+2)) 353 current._used_vars |= set([new_unique_variable]) 354 agenda.put(current.term.replace(current.variable, new_unique_variable)) 355 agenda[Categories.ALL].add(current) 356 agenda.mark_alls_fresh() 357 return _attempt_proof(agenda, accessible_vars|set([new_unique_variable]), atoms, (debug[0], debug[1]+1))

358 359

360 -class Categories:

361 ATOM = 0 362 N_ATOM = 1 363 N_EQ = 2 364 D_NEG = 3 365 N_ALL = 4 366 N_EXISTS = 5 367 AND = 6 368 N_OR = 7 369 N_IMP = 8 370 OR = 9 371 IMP = 10 372 N_AND = 11 373 IFF = 12 374 N_IFF = 13 375 EQ = 14 376 EXISTS = 15 377 ALL = 16

378

379 -def testTableau():

380 tableau_test(r'man(x)') 381 tableau_test(r'(man(x) -> man(x))') 382 tableau_test(r'(man(x) -> --man(x))') 383 tableau_test(r'-(man(x) and -man(x))') 384 tableau_test(r'(man(x) or -man(x))') 385 tableau_test(r'(man(x) -> man(x))') 386 tableau_test(r'-(man(x) and -man(x))') 387 tableau_test(r'(man(x) or -man(x))') 388 tableau_test(r'(man(x) -> man(x))') 389 tableau_test(r'(man(x) iff man(x))') 390 tableau_test(r'-(man(x) iff -man(x))') 391 tableau_test('all x.man(x)') 392 tableau_test('all x.all y.((x = y) -> (y = x))') 393 tableau_test('all x.all y.all z.(((x = y) & (y = z)) -> (x = z))') 394 tableau_test('-all x.some y.F(x,y) & some x.all y.(-F(x,y))') 395 tableau_test('some x.all y.sees(x,y)') 396 397 p1 = LogicParser().parse(r'all x.(man(x) -> mortal(x))') 398 p2 = LogicParser().parse(r'man(Socrates)') 399 c = LogicParser().parse(r'mortal(Socrates)') 400 print '%s, %s |- %s: %s' % (p1, p2, c, Tableau(c, [p1,p2]).prove()) 401 402 p1 = LogicParser().parse(r'all x.(man(x) -> walks(x))') 403 p2 = LogicParser().parse(r'man(John)') 404 c = LogicParser().parse(r'some y.walks(y)') 405 print '%s, %s |- %s: %s' % (p1, p2, c, Tableau(c, [p1,p2]).prove()) 406 407 p = LogicParser().parse(r'((x = y) & walks(y))') 408 c = LogicParser().parse(r'walks(x)') 409 print '%s |- %s: %s' % (p, c, Tableau(c, [p]).prove()) 410 411 p = LogicParser().parse(r'((x = y) & ((y = z) & (z = w)))') 412 c = LogicParser().parse(r'(x = w)') 413 print '%s |- %s: %s' % (p, c, Tableau(c, [p]).prove()) 414 415 p = LogicParser().parse(r'some e1.some e2.(believe(e1,john,e2) & walk(e2,mary))') 416 c = LogicParser().parse(r'some e0.walk(e0,mary)') 417 print '%s |- %s: %s' % (p, c, Tableau(c, [p]).prove()) 418 419 c = LogicParser().parse(r'(exists x.exists z3.((x = Mary) & ((z3 = John) & sees(z3,x))) <-> exists x.exists z4.((x = John) & ((z4 = Mary) & sees(x,z4))))') 420 print '|- %s: %s' % (c, Tableau(c, []).prove())

421 422 # p = LogicParser().parse(r'some e1.some e2.((believe e1 john e2) and (walk e2 mary))') 423 # c = LogicParser().parse(r'some x.some e3.some e4.((believe e3 x e4) and (walk e4 mary))') 424 # print '%s |- %s: %s' % (p, c, Tableau(c,[p]).prove()) 425

426 -def tableau_test(e):

427 f = LogicParser().parse(e) 428 t = ProverCommand(Tableau(), f) 429 print '|- %s: %s' % (f, t.prove())

430 431 if __name__ == '__main__': 432 testTableau() 433

Source Code for Module nltk.inference.tableau