Module for a resolution-based First Order theorem prover.
- exception nltk.inference.resolution.ProverParseError¶
- class nltk.inference.resolution.ResolutionProver¶
- ANSWER_KEY = 'ANSWER'¶
- class nltk.inference.resolution.ResolutionProverCommand¶
- __init__(goal=None, assumptions=None, prover=None)¶
goal (sem.Expression) – Input expression to prove
assumptions (list(sem.Expression)) – Input expressions to use as assumptions in the proof.
Perform the actual proof. Store the result to prevent unnecessary re-proving.
- class nltk.inference.resolution.Clause¶
- unify(other, bindings=None, used=None, skipped=None, debug=False)¶
Attempt to unify this Clause with the other, returning a list of resulting, unified, Clauses.
Clausewith which to unify
BindingDictcontaining 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
Clauseobjects. 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
list containing all the resulting
Clauseobjects that could be obtained by unification
Return True iff every term in ‘self’ is a term in ‘other’.
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’.
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)¶
Replace every instance of variable with expression across every atom in the clause
Replace every binding
bindings – A list of tuples mapping Variable Expressions to the Expressions to which they are bound.
Skolemize, clausify, and standardize the variables apart.
- class nltk.inference.resolution.BindingDict¶
binding_list – list of (
AtomicExpression) to initialize the dictionary
- nltk.inference.resolution.most_general_unification(a, b, bindings=None)¶
Find the most general unification of the two given expressions
BindingDicta starting set of bindings with which the unification must be consistent
a list of bindings
BindingException – if the Expressions cannot be unified
- class nltk.inference.resolution.DebugObject¶
- __init__(enabled=True, indent=0)¶