nltk.inference package

Submodules

nltk.inference.api module

Interfaces and base classes for theorem provers and model builders.

Prover is a standard interface for a theorem prover which tries to prove a goal from a list of assumptions.

ModelBuilder is a standard interface for a model builder. Given just a set of assumptions. the model builder tries to build a model for the assumptions. Given a set of assumptions and a goal G, the model builder tries to find a counter-model, in the sense of a model that will satisfy the assumptions plus the negation of G.

class nltk.inference.api.BaseModelBuilderCommand(modelbuilder, goal=None, assumptions=None)

Bases: nltk.inference.api.BaseTheoremToolCommand, nltk.inference.api.ModelBuilderCommand

This class holds a ModelBuilder, a goal, and a list of assumptions. When build_model() is called, the ModelBuilder is executed with the goal and assumptions.

build_model(verbose=False)

Attempt to build a model. Store the result to prevent unnecessary re-building.

get_model_builder()

Return the model builder object :return: ModelBuilder

model(format=None)

Return a string representation of the model

Parameters:simplify – bool simplify the proof? Returns:str

class nltk.inference.api.BaseProverCommand(prover, goal=None, assumptions=None)

Bases: nltk.inference.api.BaseTheoremToolCommand, nltk.inference.api.ProverCommand

This class holds a Prover, a goal, and a list of assumptions. When prove() is called, the Prover is executed with the goal and assumptions.

decorate_proof(proof_string, simplify=True)

Modify and return the proof string :param proof_string: str the proof to decorate :param simplify: bool simplify the proof? :return: str

get_prover()

Return the prover object :return: Prover

proof(simplify=True)

Return the proof string :param simplify: bool simplify the proof? :return: str

prove(verbose=False)

Perform the actual proof. Store the result to prevent unnecessary re-proving.

class nltk.inference.api.BaseTheoremToolCommand(goal=None, assumptions=None)

Bases: nltk.inference.api.TheoremToolCommand

This class holds a goal and a list of assumptions to be used in proving or model building.

add_assumptions(new_assumptions)

Add new assumptions to the assumption list.

Parameters:new_assumptions (list(sem.Expression)) – new assumptions

assumptions()

List the current assumptions.

Returns:list of Expression

goal()

Return the goal

Returns:Expression

print_assumptions()

Print the list of the current assumptions.

retract_assumptions(retracted, debug=False)

Retract assumptions from the assumption list.

Parameters:debug – If True, give warning when retracted is not present on

assumptions list. :type debug: bool :param retracted: assumptions to be retracted :type retracted: list(sem.Expression)

class nltk.inference.api.ModelBuilder

Bases: object

Interface for trying to build a model of set of formulas. Open formulas are assumed to be universally quantified. Both the goal and the assumptions are constrained to be formulas of logic.Expression.

build_model(goal=None, assumptions=None, verbose=False)

Perform the actual model building. :return: Whether a model was generated :rtype: bool

class nltk.inference.api.ModelBuilderCommand

Bases: nltk.inference.api.TheoremToolCommand

This class holds a ModelBuilder, a goal, and a list of assumptions. When build_model() is called, the ModelBuilder is executed with the goal and assumptions.

build_model(verbose=False)

Perform the actual model building. :return: A model if one is generated; None otherwise. :rtype: sem.Valuation

get_model_builder()

Return the model builder object :return: ModelBuilder

model(format=None)

Return a string representation of the model

Parameters:simplify – bool simplify the proof? Returns:str

class nltk.inference.api.ModelBuilderCommandDecorator(modelBuilderCommand)

Bases: nltk.inference.api.TheoremToolCommandDecorator, nltk.inference.api.ModelBuilderCommand

A base decorator for the ModelBuilderCommand class from which other prover command decorators can extend.

build_model(verbose=False)

Attempt to build a model. Store the result to prevent unnecessary re-building.

get_model_builder()

Return the model builder object :return: ModelBuilder

model(format=None)

Return a string representation of the model

Parameters:simplify – bool simplify the proof? Returns:str

class nltk.inference.api.ParallelProverBuilder(prover, modelbuilder)

Bases: nltk.inference.api.Prover, nltk.inference.api.ModelBuilder

This class stores both a prover and a model builder and when either prove() or build_model() is called, then both theorem tools are run in parallel. Whichever finishes first, the prover or the model builder, is the result that will be used.

class nltk.inference.api.ParallelProverBuilderCommand(prover, modelbuilder, goal=None, assumptions=None)

Bases: nltk.inference.api.BaseProverCommand, nltk.inference.api.BaseModelBuilderCommand

This command stores both a prover and a model builder and when either prove() or build_model() is called, then both theorem tools are run in parallel. Whichever finishes first, the prover or the model builder, is the result that will be used.

Because the theorem prover result is the opposite of the model builder result, we will treat self._result as meaning “proof found/no model found”.

build_model(verbose=False)

Attempt to build a model. Store the result to prevent unnecessary re-building.

prove(verbose=False)

Perform the actual proof. Store the result to prevent unnecessary re-proving.

class nltk.inference.api.Prover

Bases: object

Interface for trying to prove a goal from assumptions. Both the goal and the assumptions are constrained to be formulas of logic.Expression.

prove(goal=None, assumptions=None, verbose=False)

Returns:Whether the proof was successful or not. Return type:bool

class nltk.inference.api.ProverCommand

Bases: nltk.inference.api.TheoremToolCommand

This class holds a Prover, a goal, and a list of assumptions. When prove() is called, the Prover is executed with the goal and assumptions.

get_prover()

Return the prover object :return: Prover

proof(simplify=True)

Return the proof string :param simplify: bool simplify the proof? :return: str

prove(verbose=False)

Perform the actual proof.

class nltk.inference.api.ProverCommandDecorator(proverCommand)

Bases: nltk.inference.api.TheoremToolCommandDecorator, nltk.inference.api.ProverCommand

A base decorator for the ProverCommand class from which other prover command decorators can extend.

decorate_proof(proof_string, simplify=True)

Modify and return the proof string :param proof_string: str the proof to decorate :param simplify: bool simplify the proof? :return: str

get_prover()

Return the prover object :return: Prover

proof(simplify=True)

Return the proof string :param simplify: bool simplify the proof? :return: str

prove(verbose=False)

Perform the actual proof.

class nltk.inference.api.TheoremToolCommand

Bases: object

This class holds a goal and a list of assumptions to be used in proving or model building.

add_assumptions(new_assumptions)

Add new assumptions to the assumption list.

Parameters:new_assumptions (list(sem.Expression)) – new assumptions

assumptions()

List the current assumptions.

Returns:list of Expression

goal()

Return the goal

Returns:Expression

print_assumptions()

Print the list of the current assumptions.

retract_assumptions(retracted, debug=False)

Retract assumptions from the assumption list.

Parameters:debug – If True, give warning when retracted is not present on

assumptions list. :type debug: bool :param retracted: assumptions to be retracted :type retracted: list(sem.Expression)

class nltk.inference.api.TheoremToolCommandDecorator(command)

Bases: nltk.inference.api.TheoremToolCommand

A base decorator for the ProverCommandDecorator and ModelBuilderCommandDecorator classes from which decorators can extend.

add_assumptions(new_assumptions)

Add new assumptions to the assumption list.

Parameters:new_assumptions (list(sem.Expression)) – new assumptions

assumptions()

List the current assumptions.

Returns:list of Expression

goal()

Return the goal

Returns:Expression

print_assumptions()

Print the list of the current assumptions.

retract_assumptions(retracted, debug=False)

Retract assumptions from the assumption list.

Parameters:debug – If True, give warning when retracted is not present on

assumptions list. :type debug: bool :param retracted: assumptions to be retracted :type retracted: list(sem.Expression)

class nltk.inference.api.TheoremToolThread(command, verbose, name=None)

Bases: threading.Thread

result

run()

Method representing the thread’s activity.

You may override this method in a subclass. The standard run() method invokes the callable object passed to the object’s constructor as the target argument, if any, with sequential and keyword arguments taken from the args and kwargs arguments, respectively.

nltk.inference.discourse module

Module for incrementally developing simple discourses, and checking for semantic ambiguity, consistency and informativeness.

Many of the ideas are based on the CURT family of programs of Blackburn and Bos (see http://homepages.inf.ed.ac.uk/jbos/comsem/book1.html).

Consistency checking is carried out by using the mace module to call the Mace4 model builder. Informativeness checking is carried out with a call to Prover.prove() from the inference module.

DiscourseTester is a constructor for discourses. The basic data structure is a list of sentences, stored as self._sentences. Each sentence in the list is assigned a “sentence ID” (sid) of the form si. For example:

s0: A boxer walks
s1: Every boxer chases a girl

Each sentence can be ambiguous between a number of readings, each of which receives a “reading ID” (rid) of the form si -rj. For example:

s0 readings:

s0-r1: some x.(boxer(x) & walk(x))
s0-r0: some x.(boxerdog(x) & walk(x))

A “thread” is a list of readings, represented as a list of rids. Each thread receives a “thread ID” (tid) of the form di. For example:

d0: ['s0-r0', 's1-r0']

The set of all threads for a discourse is the Cartesian product of all the readings of the sequences of sentences. (This is not intended to scale beyond very short discourses!) The method readings(filter=True) will only show those threads which are consistent (taking into account any background assumptions).

class nltk.inference.discourse.CfgReadingCommand(gramfile=None)

Bases: nltk.inference.discourse.ReadingCommand

combine_readings(readings)

See:ReadingCommand.combine_readings()

parse_to_readings(sentence)

See:ReadingCommand.parse_to_readings()

to_fol(expression)

See:ReadingCommand.to_fol()

class nltk.inference.discourse.DiscourseTester(input, reading_command=None, background=None)

Bases: object

Check properties of an ongoing discourse.

add_background(background, verbose=False)

Add a list of background assumptions for reasoning about the discourse.

When called, this method also updates the discourse model’s set of readings and threads. :param background: Formulas which contain background information :type background: list(Expression)

add_sentence(sentence, informchk=False, consistchk=False)

Add a sentence to the current discourse.

Updates self._input and self._sentences. :param sentence: An input sentence :type sentence: str :param informchk: if True, check that the result of adding the sentence is thread-informative. Updates self._readings. :param consistchk: if True, check that the result of adding the sentence is thread-consistent. Updates self._readings.

background()

Show the current background assumptions.

expand_threads(thread_id, threads=None)

Given a thread ID, find the list of logic.Expression objects corresponding to the reading IDs in that thread.

Parameters:

• thread_id (str) – thread ID
• threads (dict) – a mapping from thread IDs to lists of reading IDs

Returns:

A list of pairs (rid, reading) where reading is the logic.Expression associated with a reading ID

Return type:

list of tuple

grammar()

Print out the grammar in use for parsing input sentences

models(thread_id=None, show=True, verbose=False)

Call Mace4 to build a model for each current discourse thread.

Parameters:

• thread_id (str) – thread ID
• show – If True, display the model that has been found.

static multiply(discourse, readings)

Multiply every thread in discourse by every reading in readings.

Given discourse = [[‘A’], [‘B’]], readings = [‘a’, ‘b’, ‘c’] , returns [[‘A’, ‘a’], [‘A’, ‘b’], [‘A’, ‘c’], [‘B’, ‘a’], [‘B’, ‘b’], [‘B’, ‘c’]]

Parameters:

• discourse (list of lists) – the current list of readings
• readings (list(Expression)) – an additional list of readings

Return type:

A list of lists

readings(sentence=None, threaded=False, verbose=True, filter=False, show_thread_readings=False)

Construct and show the readings of the discourse (or of a single sentence).

Parameters:

• sentence (str) – test just this sentence
• threaded – if True, print out each thread ID and the corresponding thread.
• filter – if True, only print out consistent thread IDs and threads.

retract_sentence(sentence, verbose=True)

Remove a sentence from the current discourse.

Updates self._input, self._sentences and self._readings. :param sentence: An input sentence :type sentence: str :param verbose: If True, report on the updated list of sentences.

sentences()

Display the list of sentences in the current discourse.

class nltk.inference.discourse.DrtGlueReadingCommand(semtype_file=None, remove_duplicates=False, depparser=None)

Bases: nltk.inference.discourse.ReadingCommand

combine_readings(readings)

See:ReadingCommand.combine_readings()

parse_to_readings(sentence)

See:ReadingCommand.parse_to_readings()

process_thread(sentence_readings)

See:ReadingCommand.process_thread()

to_fol(expression)

See:ReadingCommand.to_fol()

class nltk.inference.discourse.ReadingCommand

Bases: object

combine_readings(readings)

Parameters:readings (list(Expression)) – readings to combine Returns:one combined reading Return type:Expression

parse_to_readings(sentence)

Parameters:sentence (str) – the sentence to read

process_thread(sentence_readings)

This method should be used to handle dependencies between readings such as resolving anaphora.

Parameters:sentence_readings (list(Expression)) – readings to process Returns:the list of readings after processing Return type:list(Expression)

to_fol(expression)

Convert this expression into a First-Order Logic expression.

Parameters:expression (Expression) – an expression Returns:a FOL version of the input expression Return type:Expression

nltk.inference.discourse.demo()

nltk.inference.discourse.discourse_demo(reading_command=None)

Illustrate the various methods of DiscourseTester

nltk.inference.discourse.drt_discourse_demo(reading_command=None)

Illustrate the various methods of DiscourseTester

nltk.inference.discourse.load_fol(s)

Temporarily duplicated from nltk.sem.util. Convert a file of first order formulas into a list of Expression objects.

Parameters:s (str) – the contents of the file Returns:a list of parsed formulas. Return type:list(Expression)

nltk.inference.discourse.spacer(num=30)

nltk.inference.mace module

A model builder that makes use of the external ‘Mace4’ package.

class nltk.inference.mace.Mace(end_size=500)

Bases: nltk.inference.prover9.Prover9Parent, nltk.inference.api.ModelBuilder

class nltk.inference.mace.MaceCommand(goal=None, assumptions=None, max_models=500, model_builder=None)

Bases: nltk.inference.prover9.Prover9CommandParent, nltk.inference.api.BaseModelBuilderCommand

A MaceCommand specific to the Mace model builder. It contains a print_assumptions() method that is used to print the list of assumptions in multiple formats.

valuation

nltk.inference.mace.decode_result(found)

Decode the result of model_found()

Parameters:found (bool) – The output of model_found()

nltk.inference.mace.demo()

nltk.inference.mace.spacer(num=30)

nltk.inference.mace.test_build_model(arguments)

Try to build a nltk.sem.Valuation.

nltk.inference.mace.test_make_relation_set()

nltk.inference.mace.test_model_found(arguments)

Try some proofs and exhibit the results.

nltk.inference.mace.test_transform_output(argument_pair)

Transform the model into various Mace4 interpformat formats.

nltk.inference.nonmonotonic module

A module to perform nonmonotonic reasoning. The ideas and demonstrations in this module are based on “Logical Foundations of Artificial Intelligence” by Michael R. Genesereth and Nils J. Nilsson.

class nltk.inference.nonmonotonic.ClosedDomainProver(proverCommand)

Bases: nltk.inference.api.ProverCommandDecorator

This is a prover decorator that adds domain closure assumptions before proving.

assumptions()

List the current assumptions.

Returns:list of Expression

goal()

Return the goal

Returns:Expression

replace_quants(ex, domain)

Apply the closed domain assumption to the expression

• Domain = union([e.free()|e.constants() for e in all_expressions])

• translate “exists x.P” to “(z=d1 | z=d2 | … ) & P.replace(x,z)” OR

  “P.replace(x, d1) | P.replace(x, d2) | …”

• translate “all x.P” to “P.replace(x, d1) & P.replace(x, d2) & …”

Parameters:

• ex – Expression
• domain – set of {Variable}s

Returns:

Expression

class nltk.inference.nonmonotonic.ClosedWorldProver(proverCommand)

Bases: nltk.inference.api.ProverCommandDecorator

This is a prover decorator that completes predicates before proving.

If the assumptions contain “P(A)”, then “all x.(P(x) -> (x=A))” is the completion of “P”. If the assumptions contain “all x.(ostrich(x) -> bird(x))”, then “all x.(bird(x) -> ostrich(x))” is the completion of “bird”. If the assumptions don’t contain anything that are “P”, then “all x.-P(x)” is the completion of “P”.

walk(Socrates) Socrates != Bill + all x.(walk(x) -> (x=Socrates)) —————- -walk(Bill)

see(Socrates, John) see(John, Mary) Socrates != John John != Mary + all x.all y.(see(x,y) -> ((x=Socrates & y=John) | (x=John & y=Mary))) —————- -see(Socrates, Mary)

all x.(ostrich(x) -> bird(x)) bird(Tweety) -ostrich(Sam) Sam != Tweety + all x.(bird(x) -> (ostrich(x) | x=Tweety)) + all x.-ostrich(x) ——————- -bird(Sam)

assumptions()

List the current assumptions.

Returns:list of Expression

class nltk.inference.nonmonotonic.PredHolder

Bases: object

This class will be used by a dictionary that will store information about predicates to be used by the ClosedWorldProver.

The ‘signatures’ property is a list of tuples defining signatures for which the predicate is true. For instance, ‘see(john, mary)’ would be result in the signature ‘(john,mary)’ for ‘see’.

The second element of the pair is a list of pairs such that the first element of the pair is a tuple of variables and the second element is an expression of those variables that makes the predicate true. For instance, ‘all x.all y.(see(x,y) -> know(x,y))’ would result in “((x,y),(‘see(x,y)’))” for ‘know’.

append_prop(new_prop)

append_sig(new_sig)

unicode_repr()

Return repr(self).

validate_sig_len(new_sig)

exception nltk.inference.nonmonotonic.ProverParseError

Bases: Exception

class nltk.inference.nonmonotonic.SetHolder

Bases: list

A list of sets of Variables.

class nltk.inference.nonmonotonic.UniqueNamesProver(proverCommand)

Bases: nltk.inference.api.ProverCommandDecorator

This is a prover decorator that adds unique names assumptions before proving.

assumptions()

• Domain = union([e.free()|e.constants() for e in all_expressions])
• if “d1 = d2” cannot be proven from the premises, then add “d1 != d2”

nltk.inference.nonmonotonic.closed_domain_demo()

nltk.inference.nonmonotonic.closed_world_demo()

nltk.inference.nonmonotonic.combination_prover_demo()

nltk.inference.nonmonotonic.default_reasoning_demo()

nltk.inference.nonmonotonic.demo()

nltk.inference.nonmonotonic.get_domain(goal, assumptions)

nltk.inference.nonmonotonic.print_proof(goal, premises)

nltk.inference.nonmonotonic.unique_names_demo()

nltk.inference.prover9 module

A theorem prover that makes use of the external ‘Prover9’ package.

class nltk.inference.prover9.Prover9(timeout=60)

Bases: nltk.inference.prover9.Prover9Parent, nltk.inference.api.Prover

prover9_input(goal, assumptions)

See:Prover9Parent.prover9_input

class nltk.inference.prover9.Prover9Command(goal=None, assumptions=None, timeout=60, prover=None)

Bases: nltk.inference.prover9.Prover9CommandParent, nltk.inference.api.BaseProverCommand

A ProverCommand specific to the Prover9 prover. It contains the a print_assumptions() method that is used to print the list of assumptions in multiple formats.

decorate_proof(proof_string, simplify=True)

:see BaseProverCommand.decorate_proof()

class nltk.inference.prover9.Prover9CommandParent

Bases: object

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.

print_assumptions(output_format='nltk')

Print the list of the current assumptions.

exception nltk.inference.prover9.Prover9Exception(returncode, message)

Bases: Exception

exception nltk.inference.prover9.Prover9FatalException(returncode, message)

Bases: nltk.inference.prover9.Prover9Exception

exception nltk.inference.prover9.Prover9LimitExceededException(returncode, message)

Bases: nltk.inference.prover9.Prover9Exception

class nltk.inference.prover9.Prover9Parent

Bases: object

A common class extended by both Prover9 and Mace <mace.Mace>. It contains the functionality required to convert NLTK-style expressions into Prover9-style expressions.

binary_locations()

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.

config_prover9(binary_location, verbose=False)

prover9_input(goal, assumptions)

Returns:The input string that should be provided to the

prover9 binary. This string is formed based on the goal, assumptions, and timeout value of this object.

nltk.inference.prover9.convert_to_prover9(input)

Convert a logic.Expression to Prover9 format.

nltk.inference.prover9.demo()

nltk.inference.prover9.spacer(num=45)

nltk.inference.prover9.test_config()

nltk.inference.prover9.test_convert_to_prover9(expr)

Test that parsing works OK.

nltk.inference.prover9.test_prove(arguments)

Try some proofs and exhibit the results.

nltk.inference.resolution module

Module for a resolution-based First Order theorem prover.

class nltk.inference.resolution.BindingDict(binding_list=None)

Bases: object

unicode_repr()

Return repr(self).

exception nltk.inference.resolution.BindingException(arg)

Bases: Exception

class nltk.inference.resolution.Clause(data)

Bases: list

free()

isSubsetOf(other)

Return True iff every term in ‘self’ is a term in ‘other’.

Parameters:other – Clause Returns:bool

is_tautology()

Self is a tautology if it contains ground terms P and -P. The ground term, P, must be an exact match, ie, not using unification.

replace(variable, expression)

Replace every instance of variable with expression across every atom in the clause

Parameters:

• variable – Variable
• expression – Expression

substitute_bindings(bindings)

Replace every binding

Parameters:bindings – A list of tuples mapping Variable Expressions to the

Expressions to which they are bound :return: Clause

subsumes(other)

Return True iff ‘self’ subsumes ‘other’, this is, if there is a substitution such that every term in ‘self’ can be unified with a term in ‘other’.

Parameters:other – Clause Returns:bool

unicode_repr()

Return repr(self).

unify(other, bindings=None, used=None, skipped=None, debug=False)

Attempt to unify this Clause with the other, returning a list of resulting, unified, Clauses.

Parameters:

• other – Clause with which to unify
• bindings – BindingDict containing bindings that should be used

during the unification :param used: tuple of two lists of atoms. The first lists the atoms from ‘self’ that were successfully unified with atoms from ‘other’. The second lists the atoms from ‘other’ that were successfully unified with atoms from ‘self’. :param skipped: tuple of two Clause objects. The first is a list of all the atoms from the ‘self’ Clause that have not been unified with anything on the path. The second is same thing for the ‘other’ Clause. :param debug: bool indicating whether debug statements should print :return: list containing all the resulting Clause objects that could be obtained by unification

class nltk.inference.resolution.DebugObject(enabled=True, indent=0)

Bases: object

line(line)

exception nltk.inference.resolution.ProverParseError

Bases: Exception

class nltk.inference.resolution.ResolutionProver

Bases: nltk.inference.api.Prover

ANSWER_KEY = 'ANSWER'

class nltk.inference.resolution.ResolutionProverCommand(goal=None, assumptions=None, prover=None)

Bases: nltk.inference.api.BaseProverCommand

find_answers(verbose=False)

prove(verbose=False)

Perform the actual proof. Store the result to prevent unnecessary re-proving.

exception nltk.inference.resolution.UnificationException(a, b)

Bases: Exception

nltk.inference.resolution.clausify(expression)

Skolemize, clausify, and standardize the variables apart.

nltk.inference.resolution.demo()

nltk.inference.resolution.most_general_unification(a, b, bindings=None)

Find the most general unification of the two given expressions

Parameters:

• a – Expression
• b – Expression
• bindings – BindingDict a starting set of bindings with which the unification must be consistent

Returns:

a list of bindings

Raises:

BindingException – if the Expressions cannot be unified

nltk.inference.resolution.resolution_test(e)

nltk.inference.resolution.testResolutionProver()

nltk.inference.resolution.test_clausify()

nltk.inference.tableau module

Module for a tableau-based First Order theorem prover.

class nltk.inference.tableau.Agenda

Bases: object

clone()

mark_alls_fresh()

mark_neqs_fresh()

pop_first()

Pop the first expression that appears in the agenda

put(expression, context=None)

put_all(expressions)

put_atoms(atoms)

replace_all(old, new)

class nltk.inference.tableau.Categories

Bases: object

ALL = 20

AND = 10

APP = 4

ATOM = 0

D_NEG = 7

EQ = 18

EXISTS = 19

IFF = 16

IMP = 14

N_ALL = 8

N_AND = 15

N_APP = 5

N_ATOM = 2

N_EQ = 6

N_EXISTS = 9

N_IFF = 17

N_IMP = 12

N_OR = 11

N_PROP = 3

OR = 13

PROP = 1

class nltk.inference.tableau.Debug(verbose, indent=0, lines=None)

Bases: object

line(data, indent=0)

exception nltk.inference.tableau.ProverParseError

Bases: Exception

class nltk.inference.tableau.TableauProver

Bases: nltk.inference.api.Prover

static is_atom(e)

class nltk.inference.tableau.TableauProverCommand(goal=None, assumptions=None, prover=None)

Bases: nltk.inference.api.BaseProverCommand

nltk.inference.tableau.demo()

nltk.inference.tableau.tableau_test(c, ps=None, verbose=False)

nltk.inference.tableau.testHigherOrderTableauProver()

nltk.inference.tableau.testTableauProver()

Module contents

Classes and interfaces for theorem proving and model building.