nltk.inference.resolution module

Module for a resolution-based First Order theorem prover.

class nltk.inference.resolution.BindingDict[source]

Bases: object

__init__(binding_list=None)[source]
Parameters

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

exception nltk.inference.resolution.BindingException[source]

Bases: Exception

__init__(arg)[source]
class nltk.inference.resolution.Clause[source]

Bases: list

__init__(data)[source]
free()[source]
isSubsetOf(other)[source]

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

Parameters

other – Clause

Returns

bool

is_tautology()[source]

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)[source]

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

Parameters

  • variable – Variable

  • expression – Expression

substitute_bindings(bindings)[source]

Replace every binding

Parameters

bindings – A list of tuples mapping Variable Expressions to the Expressions to which they are bound.

Returns

Clause

subsumes(other)[source]

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)[source]

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[source]

Bases: object

__init__(enabled=True, indent=0)[source]
line(line)[source]
exception nltk.inference.resolution.ProverParseError[source]

Bases: Exception

class nltk.inference.resolution.ResolutionProver[source]

Bases: Prover

ANSWER_KEY = 'ANSWER'
class nltk.inference.resolution.ResolutionProverCommand[source]

Bases: BaseProverCommand

__init__(goal=None, assumptions=None, prover=None)[source]
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)[source]
prove(verbose=False)[source]

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

exception nltk.inference.resolution.UnificationException[source]

Bases: Exception

__init__(a, b)[source]
nltk.inference.resolution.clausify(expression)[source]

Skolemize, clausify, and standardize the variables apart.

nltk.inference.resolution.demo()[source]
nltk.inference.resolution.most_general_unification(a, b, bindings=None)[source]

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)[source]
nltk.inference.resolution.testResolutionProver()[source]
nltk.inference.resolution.test_clausify()[source]