nltk.inference.resolution

module documentation
(source)

Module for a resolution-based First Order theorem prover.

Class BindingDict No class docstring; 0/1 instance variable, 4/8 methods documented
Class Clause No class docstring; 0/2 instance variable, 6/13 methods documented
Class DebugObject Undocumented
Class ResolutionProver No class docstring; 0/1 class variable, 0/1 constant, 1/2 method documented
Class ResolutionProverCommand No class docstring; 0/3 instance variable, 2/3 methods, 1/1 static method documented
Exception BindingException Undocumented
Exception ProverParseError Undocumented
Exception UnificationException Undocumented
Function clausify Skolemize, clausify, and standardize the variables apart.
Function demo Undocumented
Function most_general_unification Find the most general unification of the two given expressions
Function resolution_test Undocumented
Function test_clausify Undocumented
Function testResolutionProver Undocumented
Function _clausify No summary
Function _complete_unify_path Undocumented
Function _iterate_first This method facilitates movement through the terms of 'self'
Function _iterate_second This method facilitates movement through the terms of 'other'
Function _mgu_var Undocumented
Function _subsumes_finalize Undocumented
Function _unify_terms This method attempts to unify two terms. Two expressions are unifiable if there exists a substitution function S such that S(a) == S(-b).
def clausify(expression): (source)

Skolemize, clausify, and standardize the variables apart.

def demo(): (source)

Undocumented

def most_general_unification(a, b, bindings=None): (source)

Find the most general unification of the two given expressions

Parameters
aExpression
bExpression
bindingsBindingDict a starting set of bindings with which the unification must be consistent
Returns
a list of bindings
Raises
BindingExceptionif the Expressions cannot be unified
def resolution_test(e): (source)

Undocumented

def test_clausify(): (source)

Undocumented

def testResolutionProver(): (source)

Undocumented

def _clausify(expression): (source)
Parameters
expressiona skolemized expression in CNF
def _complete_unify_path(first, second, bindings, used, skipped, debug): (source)

Undocumented

def _iterate_first(first, second, bindings, used, skipped, finalize_method, debug): (source)

This method facilitates movement through the terms of 'self'

def _iterate_second(first, second, bindings, used, skipped, finalize_method, debug): (source)

This method facilitates movement through the terms of 'other'

def _mgu_var(var, expression, bindings): (source)

Undocumented

def _subsumes_finalize(first, second, bindings, used, skipped, debug): (source)

Undocumented

def _unify_terms(a, b, bindings=None, used=None): (source)

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

the unification must be consistent :return: BindingDict A dictionary of the bindings required to unify :raise BindingException: If the terms cannot be unified

Parameters
aExpression
bExpression
bindingsBindingDict a starting set of bindings with which
usedUndocumented