nltk.inference.resolution module

Module for a resolution-based First Order theorem prover.

class nltk.inference.resolution.BindingDict

Bases: object

__init__(binding_list=None)

Parameters:

binding_list – list of (AbstractVariableExpression, AtomicExpression) to initialize the dictionary

exception nltk.inference.resolution.BindingException

Bases: Exception

__init__(arg)

class nltk.inference.resolution.Clause

Bases: list

__init__(data)

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.

Returns:

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

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

• 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’.

• 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.

• debug – bool indicating whether debug statements should print

Returns:

list containing all the resulting Clause objects that could be obtained by unification

class nltk.inference.resolution.DebugObject

Bases: object

__init__(enabled=True, indent=0)

line(line)

exception nltk.inference.resolution.ProverParseError

Bases: Exception

class nltk.inference.resolution.ResolutionProver

Bases: Prover

ANSWER_KEY = 'ANSWER'

class nltk.inference.resolution.ResolutionProverCommand

Bases: BaseProverCommand

__init__(goal=None, assumptions=None, prover=None)

Parameters:

• goal (sem.Expression) – Input expression to prove

• assumptions (list(sem.Expression)) – Input expressions to use as assumptions in the proof.

find_answers(verbose=False)

prove(verbose=False)

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

exception nltk.inference.resolution.UnificationException

Bases: Exception

__init__(a, b)

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()