Package nltk :: Package inference :: Module prover9

Module prover9

Classes

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

Prover9Exception

Prover9FatalException

Prover9LimitExceededException

Functions

[hide private]

convert_to_prover9(input)
Convert logic.Expressions to Prover9 format. source code

_convert_to_prover9(expression)
Convert logic.Expression to Prover9 formatted string. 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

demo()

source code

Variables

[hide private]

p9_return_codes = {0: True, 1: '(FATAL)', 2: False, 3: '(MAX_M...

Tests and Demos

arguments = [('(man(x) <-> (not (not man(x))))', []), ('(not (...

expressions = ['some x y.sees(x,y)', 'some x.(man(x) & walks(x...

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)',
...

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))',
...