Module resolution


Classes

BindingDict
BindingException
Clause
DebugObject
ProverParseError
Resolution
ResolutionCommand
UnificationException

Functions

_clausify
_complete_unify_path
_get_skolem_function
_iterate_first
_iterate_second
_mgu_var
_subsumes_finalize
_unify_terms
clausify
most_general_unification
resolution_test
skolemize
testResolution
test_clausify
to_cnf

Variables

_skolem_function_counter

[hide private]