Package nltk :: Package inference :: Module mace :: Class MaceCommand
[hide private]
[frames] | no frames]

Class MaceCommand

source code

                  object --+    
                           |    
prover9.Prover9CommandParent --+
                               |
              object --+       |
                       |       |
  api.TheoremToolCommand --+   |
                           |   |
     api.ModelBuilderCommand --+
                               |
                              MaceCommand

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

Instance Methods [hide private]
 
__init__(self, goal=None, assumptions=[], timeout=60) source code
nltk.sem.Valuation
convert2val(self)
Transform the output file into an NLTK-style Valuation.
source code
 
show_model(self, format=None)
Print out a Mace4 model using any Mace4 interpformat format.
source code
 
_transform_output(self, format)
Transform the output file into any Mace4 interpformat format.
source code

Inherited from prover9.Prover9CommandParent: print_assumptions

Inherited from api.ModelBuilderCommand: build_model

Inherited from api.TheoremToolCommand: add_assumptions, assumptions, goal, retract_assumptions

Inherited from object: __delattr__, __getattribute__, __hash__, __new__, __reduce__, __reduce_ex__, __repr__, __setattr__, __str__

Static Methods [hide private]
 
_make_model_dict(num_entities, values)
Convert a Mace4-style relation table into a dictionary.
source code
 
_make_model_var(value)
Pick an alphabetic character as identifier for an entity in the model.
source code
Instance Variables [hide private]

Inherited from api.ModelBuilderCommand (private): _modelbuilder

Inherited from api.TheoremToolCommand (private): _assumptions, _goal, _result

Properties [hide private]

Inherited from object: __class__

Method Details [hide private]

__init__(self, goal=None, assumptions=[], timeout=60)
(Constructor)

source code 
Parameters:
  • goal (logic.Expression) - Input expression to prove
  • assumptions (list of logic.Expression) - Input expressions to use as assumptions in the proof.
  • timeout (int) - number of seconds before timeout; set to 0 for no timeout.
Overrides: api.ModelBuilderCommand.__init__

convert2val(self)

source code 

Transform the output file into an NLTK-style Valuation.

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

_make_model_dict(num_entities, values)
Static Method

source code 

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) - integers that represent semantic values in a Mace4 model.

_make_model_var(value)
Static Method

source code 

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

Parameters:
  • value (int) - where to index into the list of characters

show_model(self, format=None)

source code 

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

Parameters:
  • format (str) - Output format for displaying models. Defaults to 'standard' format.

_transform_output(self, format)

source code 

Transform the output file into any Mace4 interpformat format.

Parameters:
  • format (str) - Output format for displaying models.