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

skolemize(expression, univ_scope=None)
Skolemize the expression and convert to conjunctive normal form (CNF)

source code

to_cnf(first, second)
Convert this split disjunction to conjunctive normal form (CNF)

source code

_get_skolem_function(univ_scope)
Return a skolem function over the varibles in univ_scope

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

testResolution()

source code

resolution_test(e)

source code

test_clausify()

source code

Variables

[hide private]

_skolem_function_counter = Counter()

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