nltk.inference.resolution module¶
Module for a resolution-based First Order theorem prover.
- class nltk.inference.resolution.ResolutionProver[source]¶
Bases:
nltk.inference.api.Prover
- ANSWER_KEY = 'ANSWER'¶
- class nltk.inference.resolution.ResolutionProverCommand[source]¶
Bases:
nltk.inference.api.BaseProverCommand
- __init__(goal=None, assumptions=None, prover=None)[source]¶
- Parameters
goal (sem.Expression) – Input expression to prove
assumptions (list(sem.Expression)) – Input expressions to use as assumptions in the proof.
- class nltk.inference.resolution.Clause[source]¶
Bases:
list
- unify(other, bindings=None, used=None, skipped=None, debug=False)[source]¶
Attempt to unify this Clause with the other, returning a list of resulting, unified, Clauses.
- Parameters
other –
Clause
with which to unifybindings –
BindingDict
containing bindings that should be used during the unificationused – 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
Clause
objects. 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
- Returns
list containing all the resulting
Clause
objects that could be obtained by unification
- isSubsetOf(other)[source]¶
Return True iff every term in ‘self’ is a term in ‘other’.
- Parameters
other –
Clause
- Returns
bool
- subsumes(other)[source]¶
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’.
- Parameters
other –
Clause
- Returns
bool
- is_tautology()[source]¶
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.
- nltk.inference.resolution.clausify(expression)[source]¶
Skolemize, clausify, and standardize the variables apart.
- nltk.inference.resolution.most_general_unification(a, b, bindings=None)[source]¶
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