Coverage for nltk.inference.api : 44%
Hot-keys on this page
r m x p toggle line displays
j k next/prev highlighted chunk
0 (zero) top of page
1 (one) first highlighted chunk
|
# Natural Language Toolkit: Classifier Interface # # Author: Ewan Klein <ewan@inf.ed.ac.uk> # Dan Garrette <dhgarrette@gmail.com> # # URL: <http://www.nltk.org/> # For license information, see LICENSE.TXT
Interfaces and base classes for theorem provers and model builders.
``Prover`` is a standard interface for a theorem prover which tries to prove a goal from a list of assumptions.
``ModelBuilder`` is a standard interface for a model builder. Given just a set of assumptions. the model builder tries to build a model for the assumptions. Given a set of assumptions and a goal *G*, the model builder tries to find a counter-model, in the sense of a model that will satisfy the assumptions plus the negation of *G*. """
""" Interface for trying to prove a goal from assumptions. Both the goal and the assumptions are constrained to be formulas of ``logic.Expression``. """ """ :return: Whether the proof was successful or not. :rtype: bool """ return self._prove(goal, assumptions, verbose)[0]
""" :return: Whether the proof was successful or not, along with the proof :rtype: tuple: (bool, str) """ raise NotImplementedError()
""" Interface for trying to build a model of set of formulas. Open formulas are assumed to be universally quantified. Both the goal and the assumptions are constrained to be formulas of ``logic.Expression``. """ """ Perform the actual model building. :return: Whether a model was generated :rtype: bool """ return self._build_model(goal, assumptions, verbose)[0]
""" Perform the actual model building. :return: Whether a model was generated, and the model itself :rtype: tuple(bool, sem.Valuation) """ raise NotImplementedError()
""" This class holds a goal and a list of assumptions to be used in proving or model building. """ """ Add new assumptions to the assumption list.
:param new_assumptions: new assumptions :type new_assumptions: list(sem.Expression) """ raise NotImplementedError()
""" Retract assumptions from the assumption list.
:param debug: If True, give warning when ``retracted`` is not present on assumptions list. :type debug: bool :param retracted: assumptions to be retracted :type retracted: list(sem.Expression) """ raise NotImplementedError()
""" List the current assumptions.
:return: list of ``Expression`` """ raise NotImplementedError()
""" Return the goal
:return: ``Expression`` """ raise NotImplementedError()
""" Print the list of the current assumptions. """ raise NotImplementedError()
""" This class holds a ``Prover``, a goal, and a list of assumptions. When prove() is called, the ``Prover`` is executed with the goal and assumptions. """ """ Perform the actual proof. """ raise NotImplementedError()
""" Return the proof string :param simplify: bool simplify the proof? :return: str """ raise NotImplementedError()
""" Return the prover object :return: ``Prover`` """ raise NotImplementedError()
""" This class holds a ``ModelBuilder``, a goal, and a list of assumptions. When build_model() is called, the ``ModelBuilder`` is executed with the goal and assumptions. """ """ Perform the actual model building. :return: A model if one is generated; None otherwise. :rtype: sem.Valuation """ raise NotImplementedError()
""" Return a string representation of the model
:param simplify: bool simplify the proof? :return: str """ raise NotImplementedError()
""" Return the model builder object :return: ``ModelBuilder`` """ raise NotImplementedError()
""" This class holds a goal and a list of assumptions to be used in proving or model building. """ """ :param goal: Input expression to prove :type goal: sem.Expression :param assumptions: Input expressions to use as assumptions in the proof. :type assumptions: list(sem.Expression) """
else:
""" Add new assumptions to the assumption list.
:param new_assumptions: new assumptions :type new_assumptions: list(sem.Expression) """ self._assumptions.extend(new_assumptions) self._result = None
""" Retract assumptions from the assumption list.
:param debug: If True, give warning when ``retracted`` is not present on assumptions list. :type debug: bool :param retracted: assumptions to be retracted :type retracted: list(sem.Expression) """ retracted = set(retracted) result_list = list(filter(lambda a: a not in retracted, self._assumptions)) if debug and result_list == self._assumptions: print(Warning("Assumptions list has not been changed:")) self.print_assumptions()
self._assumptions = result_list
self._result = None
""" List the current assumptions.
:return: list of ``Expression`` """
""" Return the goal
:return: ``Expression`` """
""" Print the list of the current assumptions. """ for a in self.assumptions(): print(a)
""" This class holds a ``Prover``, a goal, and a list of assumptions. When prove() is called, the ``Prover`` is executed with the goal and assumptions. """ """ :param prover: The theorem tool to execute with the assumptions :type prover: Prover :see: ``BaseTheoremToolCommand`` """ """The theorem tool to execute with the assumptions"""
""" Perform the actual proof. Store the result to prevent unnecessary re-proving. """ if self._result is None: self._result, self._proof = self._prover._prove(self.goal(), self.assumptions(), verbose) return self._result
""" Return the proof string :param simplify: bool simplify the proof? :return: str """ else:
""" Modify and return the proof string :param proof_string: str the proof to decorate :param simplify: bool simplify the proof? :return: str """
return self._prover
""" This class holds a ``ModelBuilder``, a goal, and a list of assumptions. When build_model() is called, the ``ModelBuilder`` is executed with the goal and assumptions. """ """ :param modelbuilder: The theorem tool to execute with the assumptions :type modelbuilder: ModelBuilder :see: ``BaseTheoremToolCommand`` """ self._modelbuilder = modelbuilder """The theorem tool to execute with the assumptions"""
BaseTheoremToolCommand.__init__(self, goal, assumptions)
self._model = None
""" Attempt to build a model. Store the result to prevent unnecessary re-building. """ if self._result is None: self._result, self._model = \ self._modelbuilder._build_model(self.goal(), self.assumptions(), verbose) return self._result
""" Return a string representation of the model
:param simplify: bool simplify the proof? :return: str """ if self._result is None: raise LookupError('You have to call build_model() first to ' 'get a model!') else: return self._decorate_model(self._model, format)
""" :param valuation_str: str with the model builder's output :param format: str indicating the format for displaying :return: str """ return valuation_str
return self._modelbuilder
""" A base decorator for the ``ProverCommandDecorator`` and ``ModelBuilderCommandDecorator`` classes from which decorators can extend. """ """ :param command: ``TheoremToolCommand`` to decorate """ self._command = command
#The decorator has its own versions of 'result' different from the #underlying command self._result = None
return self._command.assumptions()
return self._command.goal()
self._command.add_assumptions(new_assumptions) self._result = None
self._command.retract_assumptions(retracted, debug) self._result = None
self._command.print_assumptions()
""" A base decorator for the ``ProverCommand`` class from which other prover command decorators can extend. """ """ :param proverCommand: ``ProverCommand`` to decorate """ TheoremToolCommandDecorator.__init__(self, proverCommand)
#The decorator has its own versions of 'result' and 'proof' #because they may be different from the underlying command self._proof = None
if self._result is None: prover = self.get_prover() self._result, self._proof = prover._prove(self.goal(), self.assumptions(), verbose) return self._result
""" Return the proof string :param simplify: bool simplify the proof? :return: str """ if self._result is None: raise LookupError("You have to call prove() first to get a proof!") else: return self.decorate_proof(self._proof, simplify)
""" Modify and return the proof string :param proof_string: str the proof to decorate :param simplify: bool simplify the proof? :return: str """ return self._command.decorate_proof(proof_string, simplify)
return self._command.get_prover()
""" A base decorator for the ``ModelBuilderCommand`` class from which other prover command decorators can extend. """ """ :param modelBuilderCommand: ``ModelBuilderCommand`` to decorate """ TheoremToolCommandDecorator.__init__(self, modelBuilderCommand)
#The decorator has its own versions of 'result' and 'valuation' #because they may be different from the underlying command self._model = None
""" Attempt to build a model. Store the result to prevent unnecessary re-building. """ if self._result is None: modelbuilder = self.get_model_builder() self._result, self._model = \ modelbuilder._build_model(self.goal(), self.assumptions(), verbose) return self._result
""" Return a string representation of the model
:param simplify: bool simplify the proof? :return: str """ if self._result is None: raise LookupError('You have to call build_model() first to ' 'get a model!') else: return self._decorate_model(self._model, format)
""" Modify and return the proof string :param valuation_str: str with the model builder's output :param format: str indicating the format for displaying :return: str """ return self._command._decorate_model(valuation_str, format)
return self._command.get_prover()
""" This class stores both a prover and a model builder and when either prove() or build_model() is called, then both theorem tools are run in parallel. Whichever finishes first, the prover or the model builder, is the result that will be used. """ self._prover = prover self._modelbuilder = modelbuilder
return self._run(goal, assumptions, verbose), ''
return not self._run(goal, assumptions, verbose), ''
# Set up two thread, Prover and ModelBuilder to run in parallel tp_thread = TheoremToolThread(lambda: self._prover.prove(goal, assumptions, verbose), verbose, 'TP') mb_thread = TheoremToolThread(lambda: self._modelbuilder.build_model(goal, assumptions, verbose), verbose, 'MB')
tp_thread.start() mb_thread.start()
while tp_thread.isAlive() and mb_thread.isAlive(): # wait until either the prover or the model builder is done pass
if tp_thread.result is not None: return tp_thread.result elif mb_thread.result is not None: return not mb_thread.result else: return None
""" This command stores both a prover and a model builder and when either prove() or build_model() is called, then both theorem tools are run in parallel. Whichever finishes first, the prover or the model builder, is the result that will be used.
Because the theorem prover result is the opposite of the model builder result, we will treat self._result as meaning "proof found/no model found". """ BaseProverCommand.__init__(self, prover, goal, assumptions) BaseModelBuilderCommand.__init__(self, modelbuilder, goal, assumptions)
return self._run(verbose)
return not self._run(verbose)
# Set up two thread, Prover and ModelBuilder to run in parallel tp_thread = TheoremToolThread(lambda: BaseProverCommand.prove(self, verbose), verbose, 'TP') mb_thread = TheoremToolThread(lambda: BaseModelBuilderCommand.build_model(self, verbose), verbose, 'MB')
tp_thread.start() mb_thread.start()
while tp_thread.isAlive() and mb_thread.isAlive(): # wait until either the prover or the model builder is done pass
if tp_thread.result is not None: self._result = tp_thread.result elif mb_thread.result is not None: self._result = not mb_thread.result return self._result
threading.Thread.__init__(self) self._command = command self._result = None self._verbose = verbose self._name = name
try: self._result = self._command() if self._verbose: print('Thread %s finished with result %s at %s' % \ (self._name, self._result, time.localtime(time.time()))) except Exception as e: print(e) print('Thread %s completed abnormally' % (self._name))
def result(self): return self._result |