nltk.inference.MaceCommand

class nltk.inference.MaceCommand

Bases: Prover9CommandParent, BaseModelBuilderCommand

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.

__init__(goal=None, assumptions=None, max_models=500, model_builder=None)

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.)

property valuation

add_assumptions(new_assumptions)

Add new assumptions to the assumption list.

Parameters

new_assumptions (list(sem.Expression)) – new assumptions

assumptions()

List the current assumptions.

Returns

list of Expression

build_model(verbose=False)

Attempt to build a model. Store the result to prevent unnecessary re-building.

get_model_builder()

Return the model builder object :return: ModelBuilder

goal()

Return the goal

Returns

Expression

model(format=None)

Return a string representation of the model

Parameters

simplify – bool simplify the proof?

Returns

str

print_assumptions(output_format='nltk')

Print the list of the current assumptions.

retract_assumptions(retracted, debug=False)

Retract assumptions from the assumption list.

Parameters

• debug (bool) – If True, give warning when retracted is not present on assumptions list.

• retracted (list(sem.Expression)) – assumptions to be retracted