nltk.inference.resolution

Module resolution

Functions

_iterate_first(first, second, bindings, used, skipped, finalize_method, debug)
This method facilitates movement through the terms of 'self'

source code

_iterate_second(first, second, bindings, used, skipped, finalize_method, debug)
This method facilitates movement through the terms of 'other'

source code

_unify_terms(a, b, bindings=None, used=None)
This method attempts to unify two terms.

source code

_complete_unify_path(first, second, bindings, used, skipped, debug)

source code

_subsumes_finalize(first, second, bindings, used, skipped, debug)

source code

clausify(expression)
Skolemize, clausify, and standardize the variables apart.

source code

_clausify(expression)

source code

most_general_unification(a, b, bindings=None)
Find the most general unification of the two given expressions

source code

_mgu_var(var, expression, bindings)

source code

testResolutionProver()

source code

resolution_test(e)

source code

test_clausify()

source code

demo()

source code

Variables

[hide private]

APP = 'APP'

Function Details

[hide private]

_unify_terms(a, b, bindings=None, used=None)

source code

This method attempts to unify two terms. Two expressions are unifiable if there exists a substitution function S such that S(a) == S(-b).

Parameters:

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

Returns:

BindingDict A dictionary of the bindings required to unify @raise BindingException: If the terms cannot be unified

_clausify(expression)

source code

Parameters:

expression - a skolemized expression in CNF

most_general_unification(a, b, bindings=None)

source code

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