nltk.inference.mace.MaceCommand

class documentation

class MaceCommand(Prover9CommandParent, BaseModelBuilderCommand): (source)

Constructor: MaceCommand(goal, assumptions, max_models, model_builder)

A MaceCommand specific to the Mace model builder. It contains a print_assumptions() method that is used to print the list of assumptions in multiple formats.

Method	`__init__`	No summary
Property	`valuation`	Undocumented
Static Method	`_make_model_var`	Pick an alphabetic character as identifier for an entity in the model.
Static Method	`_make_relation_set`	Convert a Mace4-style relation table into a dictionary.
Static Method	`_make_relation_tuple`	Undocumented
Method	`_call_interpformat`	Call the `interpformat` binary with the given input.
Method	`_convert2val`	Transform the output file into an NLTK-style Valuation.
Method	`_decorate_model`	Print out a Mace4 model using any Mace4 `interpformat` format. See http://www.cs.unm.edu/~mccune/mace4/manual/ for details.
Method	`_transform_output`	Transform the output file into any Mace4 `interpformat` format.
Instance Variable	`_interpformat_bin`	Undocumented

Inherited from Prover9CommandParent:

Method print_assumptions Print the list of the current assumptions.

Inherited from BaseModelBuilderCommand (via Prover9CommandParent):

Method	`build_model`	Attempt to build a model. Store the result to prevent unnecessary re-building.
Method	`get_model_builder`	Return the model builder object :return: `ModelBuilder`
Method	`model`	Return a string representation of the model
Instance Variable	`_model`	Undocumented
Instance Variable	`_modelbuilder`	The theorem tool to execute with the assumptions
Instance Variable	`_result`	A holder for the result, to prevent unnecessary re-proving

Inherited from BaseTheoremToolCommand (via Prover9CommandParent, BaseModelBuilderCommand):

Method	`add_assumptions`	Add new assumptions to the assumption list.
Method	`assumptions`	List the current assumptions.
Method	`goal`	Return the goal
Method	`retract_assumptions`	Retract assumptions from the assumption list.
Instance Variable	`_assumptions`	Undocumented
Instance Variable	`_goal`	Undocumented

def __init__(self, goal=None, assumptions=None, max_models=500, model_builder=None): (source) ¶

overrides nltk.inference.api.BaseModelBuilderCommand.__init__

Parameters
goal:sem.Expression	Input expression to prove
assumptions:list(sem.Expression)	Input expressions to use as assumptions in the proof.
max_models:int	The maximum number of models that Mace will try before simply returning false. (Use 0 for no maximum.)
model_builder	Undocumented

@property
valuation = (source) ¶

Undocumented

@staticmethod
def _make_model_var(value): (source) ¶

Pick an alphabetic character as identifier for an entity in the model.

Parameters
value:int	where to index into the list of characters

@staticmethod
def _make_relation_set(num_entities, values): (source) ¶

Convert a Mace4-style relation table into a dictionary.

Parameters
num_entities:int	the number of entities in the model; determines the row length in the table.
values:list of int	a list of 1's and 0's that represent whether a relation holds in a Mace4 model.

@staticmethod
def _make_relation_tuple(position, values, num_entities): (source) ¶

Undocumented

def _call_interpformat(self, input_str, args=[], verbose=False): (source) ¶

Call the interpformat binary with the given input.

Parameters
input_str	A string whose contents are used as stdin.
args	A list of command-line arguments.
verbose	Undocumented
Returns
A tuple (stdout, returncode)
See Also
`config_prover9`

def _convert2val(self, valuation_str): (source) ¶

Transform the output file into an NLTK-style Valuation.

Returns
sem.Valuation	A model if one is generated; None otherwise.

def _decorate_model(self, valuation_str, format): (source) ¶

overrides nltk.inference.api.BaseModelBuilderCommand._decorate_model

Print out a Mace4 model using any Mace4 interpformat format. See http://www.cs.unm.edu/~mccune/mace4/manual/ for details.

models. Defaults to 'standard' format. :return: str

Parameters
valuation_str	str with the model builder's output
format	str indicating the format for displaying

def _transform_output(self, valuation_str, format): (source) ¶

Transform the output file into any Mace4 interpformat format.

Parameters
valuation_str	Undocumented
format:str	Output format for displaying models.

_interpformat_bin = (source) ¶

Undocumented