nltk.inference.nonmonotonic.ClosedDomainProver

class documentation

class ClosedDomainProver(ProverCommandDecorator): (source)

Constructor: ClosedDomainProver(proverCommand)

View In Hierarchy

This is a prover decorator that adds domain closure assumptions before proving.

Method assumptions List the current assumptions.
Method goal Return the goal
Method replace_quants Domain = union([e.free()|e.constants() for e in all_expressions])

Inherited from ProverCommandDecorator:

Method __init__ No summary
Method decorate_proof Modify and return the proof string :param proof_string: str the proof to decorate :param simplify: bool simplify the proof? :return: str
Method get_prover Return the prover object :return: Prover
Method proof Return the proof string :param simplify: bool simplify the proof? :return: str
Method prove Perform the actual proof.
Instance Variable _proof Undocumented
Instance Variable _result Undocumented

Inherited from TheoremToolCommandDecorator (via ProverCommandDecorator):

Method add_assumptions Add new assumptions to the assumption list.
Method print_assumptions Print the list of the current assumptions.
Method retract_assumptions Retract assumptions from the assumption list.
Instance Variable _command Undocumented
def assumptions(self): (source)
overrides nltk.inference.api.TheoremToolCommandDecorator.assumptions

List the current assumptions.

Returns
list of Expression
def goal(self): (source)
overrides nltk.inference.api.TheoremToolCommandDecorator.goal

Return the goal

Returns
Expression
def replace_quants(self, ex, domain): (source)

Apply the closed domain assumption to the expression
  • Domain = union([e.free()|e.constants() for e in all_expressions])
  • translate "exists x.P" to "(z=d1 | z=d2 | ... ) & P.replace(x,z)" OR
    "P.replace(x, d1) | P.replace(x, d2) | ..."
  • translate "all x.P" to "P.replace(x, d1) & P.replace(x, d2) & ..."

Parameters
exExpression
domainset of {Variable}s
Returns
Expression