nltk.inference.prover9

1 # Natural Language Toolkit: Interface to the Prover9 Theorem Prover 2 # 3 # Author: Dan Garrette <[email protected]> 4 # Ewan Klein <[email protected]> 5 6 # URL: <http://nltk.org> 7 # For license information, see LICENSE.TXT 8 9 import os 10 import tempfile 11 import subprocess 12 from string import join 13 14 from nltk.sem import logic 15 from nltk.sem.logic import LogicParser 16 17 from nltk.internals import deprecated, Deprecated, find_binary 18 19 from api import ProverCommand, Prover 20 21 """ 22 A theorem prover that makes use of the external 'Prover9' package. 23 """ 24 # 25 # Following is not yet used. Return code for 2 actually realized as 512. 26 # 27 p9_return_codes = { 28 0: True, 29 1: "(FATAL)", #A fatal error occurred (user's syntax error). 30 2: False, # (SOS_EMPTY) Prover9 ran out of things to do 31 # (sos list exhausted). 32 3: "(MAX_MEGS)", # The max_megs (memory limit) parameter was exceeded. 33 4: "(MAX_SECONDS)", # The max_seconds parameter was exceeded. 34 5: "(MAX_GIVEN)", # The max_given parameter was exceeded. 35 6: "(MAX_KEPT)", # The max_kept parameter was exceeded. 36 7: "(ACTION)", # A Prover9 action terminated the search. 37 101: "(SIGSEGV)", # Prover9 crashed, most probably due to a bug. 38 } 39 40 ###################################################################### 41 #{ Configuration 42 ###################################################################### 43 44 _prover9_bin = None 45 _prooftrans_bin = None 46 _mace4_bin = None 47 _interpformat_bin = None

48 -def config_prover9(bin=None):

49 """ 50 Configure NLTK's interface to the C{prover9} package. This 51 searches for a directory containing the executables for 52 C{prover9}, C{mace4}, C{prooftrans}, and C{interpformat}. 53 54 @param bin: The full path to the C{prover9} binary. If not 55 specified, then nltk will search the system for a C{prover9} 56 binary; and if one is not found, it will raise a 57 C{LookupError} exception. 58 @type bin: C{string} 59 """ 60 # Find the prover9 binary. 61 prover9_bin = find_binary('prover9', bin, 62 searchpath=prover9_path, env_vars=['PROVER9HOME'], 63 url='http://www.cs.unm.edu/~mccune/prover9/', 64 verbose=False) 65 66 # Make sure that mace4 and prooftrans are available, too. 67 basedir = os.path.split(prover9_bin)[0] 68 mace4_bin = os.path.join(basedir, 'mace4') 69 prooftrans_bin = os.path.join(basedir, 'prooftrans') 70 interpformat_bin = os.path.join(basedir, 'interpformat') 71 if not os.path.isfile(mace4_bin): 72 raise ValueError('prover9 was found, but mace4 was not -- ' 73 'incomplete prover9 installation?') 74 if not os.path.isfile(prooftrans_bin): 75 raise ValueError('prover9 was found, but prooftrans was not -- ' 76 'incomplete prover9 installation?') 77 if not os.path.isfile(interpformat_bin): 78 raise ValueError('prover9 was found, but interpformat was not -- ' 79 'incomplete prover9 installation?') 80 81 # Save the locations of all three binaries. 82 global _prover9_bin, _prooftrans_bin, _mace4_bin, _interpformat_bin 83 _prover9_bin = prover9_bin 84 _mace4_bin = mace4_bin 85 _prooftrans_bin = prooftrans_bin 86 _interpformat_bin = interpformat_bin

87 88 #: A list of directories that should be searched for the prover9 89 #: executables. This list is used by L{config_prover9} when searching 90 #: for the prover9 executables. 91 prover9_path = ['/usr/local/bin/prover9', 92 '/usr/local/bin/prover9/bin', 93 '/usr/local/bin', 94 '/usr/bin', 95 '/usr/local/prover9', 96 '/usr/local/share/prover9'] 97 98 ###################################################################### 99 #{ Interface to Binaries 100 ###################################################################### 101

102 -def call_prover9(input_str, args=[]):

103 """ 104 Call the C{prover9} binary with the given input. 105 106 @param input_str: A string whose contents are used as stdin. 107 @param args: A list of command-line arguments. 108 @return: A tuple (stdout, returncode) 109 @see: L{config_prover9} 110 """ 111 if _prover9_bin is None: 112 config_prover9() 113 114 # Call prover9 via a subprocess 115 cmd = [_prover9_bin] + args 116 p = subprocess.Popen(cmd, stdout=subprocess.PIPE, 117 stderr=subprocess.STDOUT, 118 stdin=subprocess.PIPE) 119 (stdout, stderr) = p.communicate(input_str) 120 return (stdout, p.returncode)

121

122 -def call_prooftrans(input_str, args=[]):

123 """ 124 Call the C{prooftrans} binary with the given input. 125 126 @param input_str: A string whose contents are used as stdin. 127 @param args: A list of command-line arguments. 128 @return: A tuple (stdout, returncode) 129 @see: L{config_prover9} 130 """ 131 if _prooftrans_bin is None: 132 config_prover9() 133 134 # Call prooftrans via a subprocess 135 cmd = [_prooftrans_bin] + args 136 p = subprocess.Popen(cmd, stdout=subprocess.PIPE, 137 stderr=subprocess.STDOUT, 138 stdin=subprocess.PIPE) 139 (stdout, stderr) = p.communicate(input_str) 140 return (stdout, p.returncode)

141

142 -def call_mace4(input_str, args=[]):

143 """ 144 Call the C{mace4} binary with the given input. 145 146 @param input_str: A string whose contents are used as stdin. 147 @param args: A list of command-line arguments. 148 @return: A tuple (stdout, returncode) 149 @see: L{config_prover9} 150 """ 151 if _mace4_bin is None: 152 config_prover9() 153 154 # Call mace4 via a subprocess 155 cmd = [_mace4_bin] + args 156 p = subprocess.Popen(cmd, 157 stdout=subprocess.PIPE, 158 stderr=subprocess.STDOUT, 159 stdin=subprocess.PIPE) 160 (stdout, stderr) = p.communicate(input_str) 161 return (stdout, p.returncode)

162

163 -def call_interpformat(input_str, args=[]):

164 """ 165 Call the C{interpformat} binary with the given input. 166 167 @param input_str: A string whose contents are used as stdin. 168 @param args: A list of command-line arguments. 169 @return: A tuple (stdout, returncode) 170 @see: L{config_prover9} 171 """ 172 if _interpformat_bin is None: 173 config_prover9() 174 175 # Call interpformat via a subprocess 176 cmd = [_interpformat_bin] + args 177 p = subprocess.Popen(cmd, stdout=subprocess.PIPE, 178 stderr=subprocess.STDOUT, 179 stdin=subprocess.PIPE) 180 (stdout, stderr) = p.communicate(input_str) 181 return (stdout, p.returncode)

182 183 ###################################################################### 184 #{ Base Class 185 ###################################################################### 186

187 -class Prover9CommandParent(object):

188 """ 189 A common base class used by both L{Prover9Command} and L{MaceCommand 190 <mace.MaceCommand>}, which is responsible for maintaining a goal and a 191 set of assumptions, and generating prover9-style input files from 192 them. 193 """

194 - def print_assumptions(self, output_format='nltk'):

195 """ 196 Print the list of the current assumptions. 197 """ 198 if output_format.lower() == 'nltk': 199 for a in self.assumptions(): 200 print a 201 elif output_format.lower() == 'prover9': 202 for a in convert_to_prover9(self.assumptions()): 203 print a 204 else: 205 raise NameError("Unrecognized value for 'output_format': %s" % 206 output_format)

207

208 -class Prover9Command(Prover9CommandParent, ProverCommand):

209 """ 210 A L{ProverCommand} specific to the L{Prover9} prover. It contains 211 the a print_assumptions() method that is used to print the list 212 of assumptions in multiple formats. 213 """

214 - def __init__(self, goal=None, assumptions=[], timeout=60):

215 """ 216 @param goal: Input expression to prove 217 @type goal: L{logic.Expression} 218 @param assumptions: Input expressions to use as assumptions in 219 the proof. 220 @type assumptions: C{list} of L{logic.Expression} 221 @param timeout: number of seconds before timeout; set to 0 for 222 no timeout. 223 @type timeout: C{int} 224 """ 225 ProverCommand.__init__(self, Prover9(timeout), goal, assumptions)

226

227 - def show_proof(self, simplify=True):

228 """ 229 Print out a Prover9 proof. 230 231 @parameter simplify: if C{True}, simplify the output file 232 using Prover9's C{prooftrans}. 233 @type simplify: C{bool} 234 """ 235 if self._result is None: 236 raise LookupError("You have to call prove() first to get a proof!") 237 238 if simplify: 239 print call_prooftrans(self._proof, ['striplabels'])[0].rstrip() 240 else: 241 print self._proof.rstrip()

242 243

244 -class Prover9Parent(object):

245 """ 246 A common class extended by both L{Prover9} and L{Mace <mace.Mace>}. 247 It contains the functionality required to convert NLTK-style 248 expressions into Prover9-style expressions. 249 """

250 - def __init__(self, timeout=60):

251 self._timeout = timeout 252 """The timeout value for prover9. If a proof can not be found 253 in this amount of time, then prover9 will return false. 254 (Use 0 for no timeout.)"""

255

256 - def prover9_input(self, goal, assumptions):

257 """ 258 @return: The input string that should be provided to the 259 prover9 binary. This string is formed based on the goal, 260 assumptions, and timeout value of this object. 261 """ 262 s = '' 263 if self._timeout > 0: 264 s += 'assign(max_seconds, %d).\n' % self._timeout 265 266 if assumptions: 267 s += 'formulas(assumptions).\n' 268 for p9_assumption in convert_to_prover9(assumptions): 269 s += ' %s.\n' % p9_assumption 270 s += 'end_of_list.\n\n' 271 272 if goal: 273 s += 'formulas(goals).\n' 274 s += ' %s.\n' % convert_to_prover9(goal) 275 s += 'end_of_list.\n\n' 276 277 return s

278

279 -def convert_to_prover9(input):

280 """ 281 Convert C{logic.Expression}s to Prover9 format. 282 """ 283 if isinstance(input, list): 284 result = [] 285 for s in input: 286 try: 287 result.append(s.simplify().str(logic.Tokens.PROVER9)) 288 except AssertionError: 289 print 'input %s cannot be converted to Prover9 input syntax' % input 290 return result 291 else: 292 try: 293 return input.simplify().str(logic.Tokens.PROVER9) 294 except AssertionError: 295 print 'input %s cannot be converted to Prover9 input syntax' % input

296 297 298 ###################################################################### 299 #{ Prover9 300 ###################################################################### 301

302 -class Prover9(Prover9Parent, Prover):

303 _proof = None #: text output from running prover9 304

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

306 """ 307 Use Prover9 to prove a theorem. 308 @return: A pair whose first element is a boolean indicating if the 309 proof was successful (i.e. returns value of 0) and whose second element 310 is the output of the prover. 311 """ 312 stdout, returncode = call_prover9(self.prover9_input(goal, 313 assumptions)) 314 return (returncode == 0, stdout)

315 316 ###################################################################### 317 #{ Tests and Demos 318 ###################################################################### 319

320 -def test_config():

321 322 a = LogicParser().parse('(walk(j) & sing(j))') 323 g = LogicParser().parse('walk(j)') 324 p = Prover9Command(g, assumptions=[a]) 325 p._executable_path = None 326 p.prover9_search=[] 327 p.prove() 328 #config_prover9('/usr/local/bin') 329 print p.prove() 330 p.show_proof()

331

332 -def test_convert_to_prover9(expr):

333 """ 334 Test that parsing works OK. 335 """ 336 for t in expr: 337 e = LogicParser().parse(t) 338 print convert_to_prover9(e)

339

340 -def test_prove(arguments):

341 """ 342 Try some proofs and exhibit the results. 343 """ 344 for (goal, assumptions) in arguments: 345 g = LogicParser().parse(goal) 346 alist = [LogicParser().parse(a) for a in assumptions] 347 p = Prover9Command(g, assumptions=alist).prove() 348 for a in alist: 349 print ' %s' % a 350 print '|- %s: %s\n' % (g, p)

351 352 arguments = [ 353 ('(man(x) <-> (not (not man(x))))', []), 354 ('(not (man(x) & (not man(x))))', []), 355 ('(man(x) | (not man(x)))', []), 356 ('(man(x) & (not man(x)))', []), 357 ('(man(x) -> man(x))', []), 358 ('(not (man(x) & (not man(x))))', []), 359 ('(man(x) | (not man(x)))', []), 360 ('(man(x) -> man(x))', []), 361 ('(man(x) <-> man(x))', []), 362 ('(not (man(x) <-> (not man(x))))', []), 363 ('mortal(Socrates)', ['all x.(man(x) -> mortal(x))', 'man(Socrates)']), 364 ('((all x.(man(x) -> walks(x)) & man(Socrates)) -> some y.walks(y))', []), 365 ('(all x.man(x) -> all x.man(x))', []), 366 ('some x.all y.sees(x,y)', []), 367 ('some e3.(walk(e3) & subj(e3, mary))', 368 ['some e1.(see(e1) & subj(e1, john) & some e2.(pred(e1, e2) & walk(e2) & subj(e2, mary)))']), 369 ('some x e1.(see(e1) & subj(e1, x) & some e2.(pred(e1, e2) & walk(e2) & subj(e2, mary)))', 370 ['some e1.(see(e1) & subj(e1, john) & some e2.(pred(e1, e2) & walk(e2) & subj(e2, mary)))']) 371 ] 372 373 expressions = [r'some x y.sees(x,y)', 374 r'some x.(man(x) & walks(x))', 375 r'\x.(man(x) & walks(x))', 376 r'\x y.sees(x,y)', 377 r'walks(john)', 378 r'\x.big(x, \y.mouse(y))', 379 r'(walks(x) & (runs(x) & (threes(x) & fours(x))))', 380 r'(walks(x) -> runs(x))', 381 r'some x.(PRO(x) & sees(John, x))', 382 r'some x.(man(x) & (not walks(x)))', 383 r'all x.(man(x) -> walks(x))'] 384

385 -def spacer(num=45):

386 print '-' * num

387 388 if __name__ == '__main__': 389 print "Testing configuration" 390 spacer() 391 test_config() 392 print 393 print "Testing conversion to Prover9 format" 394 spacer() 395 test_convert_to_prover9(expressions) 396 print 397 print "Testing proofs" 398 spacer() 399 test_prove(arguments) 400

Source Code for Module nltk.inference.prover9