Home       Trees       Indices       Help   
nltk 0.9.5
Package nltk :: Package inference :: Module prover9
[hide private]
[frames] | no frames]

Module prover9

source code

Classes [hide private]
    Base Class
  Prover9CommandParent
A common base class used by both Prover9Command and MaceCommand, which is responsible for maintaining a goal and a set of assumptions, and generating prover9-style input files from them.
  Prover9Command
A ProverCommand specific to the Prover9 prover.
  Prover9Parent
A common class extended by both Prover9 and Mace.
    Prover9
  Prover9
Functions [hide private]
    Configuration
 
config_prover9(bin=None)
Configure NLTK's interface to the prover9 package.		 source code
    Interface to Binaries
 
call_prover9(input_str, args=[])
Call the prover9 binary with the given input.		 source code
 
call_prooftrans(input_str, args=[])
Call the prooftrans binary with the given input.		 source code
 
call_mace4(input_str, args=[])
Call the mace4 binary with the given input.		 source code
 
call_interpformat(input_str, args=[])
Call the interpformat binary with the given input.		 source code
    Base Class
 
convert_to_prover9(input)
Convert logic.Expressions to Prover9 format.		 source code
    Tests and Demos
 
test_config() source code
 
test_convert_to_prover9(expr)
Test that parsing works OK.		 source code
 
test_prove(arguments)
Try some proofs and exhibit the results.		 source code
 
spacer(num=45) source code
Variables [hide private]
  p9_return_codes = {0: True, 1: '(FATAL)', 2: False, 3: '(MAX_M...
    Configuration
  _prover9_bin = None
  _prooftrans_bin = None
  _mace4_bin = None
  _interpformat_bin = None
  prover9_path = ['/usr/local/bin/prover9', '/usr/local/bin/prov...
A list of directories that should be searched for the prover9 executables.
    Tests and Demos
  arguments = [('(man(x) <-> (not (not man(x))))', []), ('(not (...
  expressions = ['some x y.sees(x,y)', 'some x.(man(x) & walks(x...
Function Details [hide private]

config_prover9(bin=None)

source code 

Configure NLTK's interface to the prover9 package. This searches for a directory containing the executables for prover9, mace4, prooftrans, and interpformat.

Parameters:
  • bin (string) - The full path to the prover9 binary. If not specified, then nltk will search the system for a prover9 binary; and if one is not found, it will raise a LookupError exception.

call_prover9(input_str, args=[])

source code 

Call the prover9 binary with the given input.

Parameters:
  • input_str - A string whose contents are used as stdin.
  • args - A list of command-line arguments.
Returns:
A tuple (stdout, returncode)

See Also: config_prover9

call_prooftrans(input_str, args=[])

source code 

Call the prooftrans binary with the given input.

Parameters:
  • input_str - A string whose contents are used as stdin.
  • args - A list of command-line arguments.
Returns:
A tuple (stdout, returncode)

See Also: config_prover9

call_mace4(input_str, args=[])

source code 

Call the mace4 binary with the given input.

Parameters:
  • input_str - A string whose contents are used as stdin.
  • args - A list of command-line arguments.
Returns:
A tuple (stdout, returncode)

See Also: config_prover9

call_interpformat(input_str, args=[])

source code 

Call the interpformat binary with the given input.

Parameters:
  • input_str - A string whose contents are used as stdin.
  • args - A list of command-line arguments.
Returns:
A tuple (stdout, returncode)

See Also: config_prover9


Variables Details [hide private]

p9_return_codes

Value:
{0: True,
 1: '(FATAL)',
 2: False,
 3: '(MAX_MEGS)',
 4: '(MAX_SECONDS)',
 5: '(MAX_GIVEN)',
 6: '(MAX_KEPT)',
 7: '(ACTION)',
...

prover9_path

A list of directories that should be searched for the prover9 executables. This list is used by config_prover9 when searching for the prover9 executables.

Value:
['/usr/local/bin/prover9',
 '/usr/local/bin/prover9/bin',
 '/usr/local/bin',
 '/usr/bin',
 '/usr/local/prover9',
 '/usr/local/share/prover9']

arguments

Value:
[('(man(x) <-> (not (not man(x))))', []),
 ('(not (man(x) & (not man(x))))', []),
 ('(man(x) | (not man(x)))', []),
 ('(man(x) & (not man(x)))', []),
 ('(man(x) -> man(x))', []),
 ('(not (man(x) & (not man(x))))', []),
 ('(man(x) | (not man(x)))', []),
 ('(man(x) -> man(x))', []),
...

expressions

Value:
['some x y.sees(x,y)',
 'some x.(man(x) & walks(x))',
 '\\x.(man(x) & walks(x))',
 '\\x y.sees(x,y)',
 'walks(john)',
 '\\x.big(x, \\y.mouse(y))',
 '(walks(x) & (runs(x) & (threes(x) & fours(x))))',
 '(walks(x) -> runs(x))',
...

   Home       Trees       Indices       Help   
nltk 0.9.5
Generated by Epydoc 3.0beta1 on Wed Aug 27 15:08:50 2008 http://epydoc.sourceforge.net