Module Expr Str ImportFrom alias Import alias Import alias ImportFrom alias ImportFrom alias alias ImportFrom alias alias ImportFrom alias alias ClassDef bases NameLoad NameLoad body Expr Str Assign NameStore NameLoad FunctionDef arguments args NameParam NameParam NameParam NameParam NameParam defaults NameLoad NameLoad Num NameLoad body Expr Str If CompareIsNot NameLoad NameLoad body Assert Call NameLoad NameLoad NameLoad orelse Assign NameStore Call NameLoad NameLoad Expr Call AttributeLoad NameLoad attr NameLoad NameLoad NameLoad NameLoad decorator_list FunctionDef arguments args NameParam defaults body Return Call AttributeLoad NameLoad attr Str decorator_list NameLoad FunctionDef arguments args NameParam NameParam defaults body Expr Str Assign NameStore Call AttributeLoad NameLoad attr NameLoad Str Assign NameStore ListLoad For NameStore Call AttributeLoad NameLoad attr NameLoad body Assign NameStore Call AttributeLoad NameLoad attr If Call AttributeLoad NameLoad attr Str body Assign NameStore Call NameLoad Call AttributeLoad SubscriptLoad NameLoad Slice BinOpAdd Call AttributeLoad NameLoad attr Str Num Call AttributeLoad NameLoad attr Str attr orelse If BoolOpAnd Call AttributeLoad NameLoad attr Str CompareEq Call AttributeLoad NameLoad attr Str Num body Assign NameStore Call AttributeLoad SubscriptLoad NameLoad Slice BinOpAdd Call AttributeLoad NameLoad attr Str Num Call AttributeLoad NameLoad attr Str attr If Call NameLoad NameLoad body Assign NameStore Call AttributeLoad NameLoad attr Assign NameStore Call NameLoad Call AttributeLoad SubscriptLoad NameLoad Slice BinOpAdd Call AttributeLoad NameLoad attr Str Num Call AttributeLoad NameLoad attr Str attr Expr Call AttributeLoad NameLoad attr TupleLoad NameLoad Call AttributeLoad NameLoad attr NameLoad orelse If Call AttributeLoad NameLoad attr Str body Assign NameStore SubscriptLoad NameLoad Slice BinOpAdd Call AttributeLoad NameLoad attr Str Num If CompareIn Str NameLoad body Assign NameStore Call AttributeLoad SubscriptLoad NameLoad Slice Call AttributeLoad NameLoad attr Str attr Assign NameStore ListComp Call NameLoad Call AttributeLoad NameLoad attr comprehension NameStore Call AttributeLoad SubscriptLoad NameLoad Slice BinOpAdd Call AttributeLoad NameLoad attr Str Num Call AttributeLoad NameLoad attr Str attr Str Expr Call AttributeLoad NameLoad attr TupleLoad NameLoad Call AttributeLoad NameLoad attr NameLoad NameLoad orelse Assign NameStore Call AttributeLoad SubscriptLoad NameLoad Slice Call AttributeLoad NameLoad attr Str attr Assign NameStore Call NameLoad Call AttributeLoad SubscriptLoad NameLoad Slice BinOpAdd Call AttributeLoad NameLoad attr Str Num Call AttributeLoad NameLoad attr Str attr Expr Call AttributeLoad NameLoad attr TupleLoad NameLoad CompareEq NameLoad Num Return Call NameLoad NameLoad decorator_list FunctionDef arguments args NameParam NameParam defaults body Expr Str Assign NameStore Call NameLoad For NameStore ListComp NameLoad comprehension TupleStore NameStore NameStore Call NameLoad NameLoad CompareEq NameLoad Num body Expr Call AttributeLoad NameLoad attr Call NameLoad Call AttributeLoad NameLoad attr NameLoad NameLoad NameLoad Return NameLoad decorator_list NameLoad FunctionDef arguments args NameParam NameParam NameParam defaults body If CompareEq Call NameLoad NameLoad Num body Return ListLoad orelse Assign NameStore BinOpFloorDiv Call NameLoad NameLoad NameLoad Assign NameStore BinOpFloorDiv NameLoad NameLoad Assign NameStore Call NameLoad BinOpMod NameLoad NameLoad Assign NameStore SubscriptLoad NameLoad Slice BinOpMult NameLoad NameLoad BinOpMult BinOpAdd NameLoad Num NameLoad Return BinOpAdd ListLoad Call AttributeLoad NameLoad attr NameLoad Call AttributeLoad NameLoad attr NameLoad NameLoad NameLoad decorator_list NameLoad FunctionDef arguments args NameParam defaults body Expr Str Assign NameStore SubscriptLoad ListLoad Str Str Str Str Str Str Str Str Str Str Str Str Str Str Str Str Str Str Str Str Str Str Str Str Str Str Index NameLoad Assign NameStore BinOpFloorDiv NameLoad Num Return IfExp CompareGt NameLoad Num BinOpAdd NameLoad Call NameLoad NameLoad NameLoad decorator_list NameLoad FunctionDef arguments args NameParam NameParam NameParam defaults body Expr Str If UnaryOpNot NameLoad body Return NameLoad orelse If CompareEq NameLoad Str body Return Call AttributeLoad NameLoad attr NameLoad orelse Return Call AttributeLoad NameLoad attr NameLoad NameLoad decorator_list FunctionDef arguments args NameParam NameParam NameParam defaults body Expr Str If CompareIn NameLoad ListLoad Str Str Str Str Str Str Str Str body Return SubscriptLoad Call AttributeLoad NameLoad attr NameLoad ListLoad NameLoad Index Num orelse Raise Call NameLoad Str decorator_list FunctionDef arguments args NameParam NameParam NameParam NameParam defaults ListLoad NameLoad body Expr Str If CompareIs AttributeLoad NameLoad attr NameLoad body Assign AttributeStore NameLoad attr Call AttributeLoad AttributeLoad NameLoad attr attr Str NameLoad Return Call AttributeLoad AttributeLoad NameLoad attr attr NameLoad AttributeLoad NameLoad attr NameLoad NameLoad decorator_list decorator_list ClassDef bases NameLoad NameLoad body Assign NameStore NameLoad FunctionDef arguments args NameParam NameParam defaults Num body Assign AttributeStore NameLoad attr NameLoad Expr Str decorator_list FunctionDef arguments args NameParam NameParam NameParam NameParam defaults NameLoad NameLoad NameLoad body Expr Str If UnaryOpNot NameLoad body Assign NameStore ListLoad Assign TupleStore NameStore NameStore Call AttributeLoad NameLoad attr Call AttributeLoad NameLoad attr NameLoad NameLoad keyword NameLoad Return TupleLoad CompareEq NameLoad Num NameLoad decorator_list FunctionDef arguments args NameParam NameParam NameParam NameParam defaults ListLoad NameLoad body Expr Str If CompareIs AttributeLoad NameLoad attr NameLoad body Assign AttributeStore NameLoad attr Call AttributeLoad NameLoad attr Str NameLoad Assign NameStore Str If CompareGt AttributeLoad NameLoad attr Num body AugAssignAdd NameStore BinOpMod Str AttributeLoad NameLoad attr AugAssignAdd NameStore NameLoad Return Call AttributeLoad NameLoad attr NameLoad AttributeLoad NameLoad attr NameLoad NameLoad decorator_list decorator_list FunctionDef arguments args NameParam defaults Num body Expr Call NameLoad BinOpMult Str NameLoad decorator_list FunctionDef arguments args NameParam defaults body Expr Str Return SubscriptLoad Dict NameLoad NameLoad NameLoad Str Str Str Index NameLoad decorator_list FunctionDef arguments args NameParam defaults body Expr Str For TupleStore NameStore NameStore NameLoad body Assign NameStore Call AttributeLoad NameLoad attr NameLoad Assign NameStore ListComp Call AttributeLoad NameLoad attr NameLoad comprehension NameStore NameLoad Assign NameStore Call NameLoad NameLoad keyword NameLoad keyword Num Assign NameStore Call AttributeLoad NameLoad attr For NameStore NameLoad body Expr Call NameLoad BinOpMod Str NameLoad Expr Call NameLoad BinOpMod Str TupleLoad NameLoad Call NameLoad NameLoad decorator_list FunctionDef arguments args NameParam defaults body Expr Str Assign NameStore Call AttributeLoad NameLoad attr Str Assign NameStore ListComp Call AttributeLoad NameLoad attr NameLoad comprehension NameStore ListLoad Str Str Str Str Str Str Assign NameStore Call NameLoad NameLoad keyword NameLoad Expr Call AttributeLoad NameLoad attr Expr Call NameLoad Expr Call NameLoad Str Expr Call NameLoad For NameStore NameLoad body Expr Call NameLoad BinOpMod Str NameLoad Expr Call NameLoad BinOpMod Str TupleLoad NameLoad Call NameLoad Call AttributeLoad NameLoad attr Expr Call NameLoad Expr Call NameLoad Str Expr Call NameLoad Expr Call NameLoad AttributeLoad NameLoad attr Str decorator_list FunctionDef arguments args NameParam defaults body Expr Str Assign NameStore Call AttributeLoad NameLoad attr SubscriptLoad NameLoad Index Num Assign NameStore ListComp Call AttributeLoad NameLoad attr NameLoad comprehension NameStore SubscriptLoad NameLoad Index Num Assign NameStore Call NameLoad NameLoad keyword NameLoad Expr Call AttributeLoad NameLoad attr For NameStore NameLoad body Expr Call NameLoad BinOpMod Str NameLoad Expr Call NameLoad BinOpMod Str TupleLoad NameLoad Call AttributeLoad NameLoad attr For NameStore ListLoad Str Str Str Str body Expr Call NameLoad Expr Call NameLoad BinOpMod Str NameLoad Expr Call NameLoad Expr Call NameLoad Call AttributeLoad NameLoad attr keyword NameLoad decorator_list FunctionDef arguments args defaults body Expr Call NameLoad CompareEq Call AttributeLoad NameLoad attr keyword Num keyword ListLoad Num Num Num Call NameLoad ListLoad TupleLoad Str TupleLoad Str Expr Call NameLoad CompareEq Call AttributeLoad NameLoad attr keyword Num keyword ListLoad Num Num Num Num Num Num Num Num Num Call NameLoad ListLoad TupleLoad Str Str Expr Call NameLoad CompareEq Call AttributeLoad NameLoad attr keyword Num keyword ListLoad Num Num Num Num Num Num Num Num Call NameLoad ListLoad TupleLoad Str Str Str TupleLoad Str Str Str decorator_list Assign NameStore ListLoad TupleLoad Str ListLoad Str Str TupleLoad Str ListLoad Str Str FunctionDef arguments args defaults body Expr Call NameLoad NameLoad Expr Call NameLoad NameLoad Expr Call NameLoad SubscriptLoad NameLoad Index Num decorator_list If CompareEq NameLoad Str body Expr Call NameLoad
N/A N/A 
A model builder that makes use of the external 'Mace4' package.
 __future__ print_function N/A os N/A tempfile nltk.sem.logic is_indvar nltk.sem Valuation Expression nltk.inference.api ModelBuilder BaseModelBuilderCommand nltk.inference.prover9 Prover9CommandParent Prover9Parent MaceCommand N/A Prover9CommandParent BaseModelBuilderCommand N/A N/A 
    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.
     N/A _interpformat_bin None __init__ N/A N/A self goal assumptions max_models model_builder N/A None None 500 None N/A N/A 
        :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)
        :param max_models: The maximum number of models that Mace will try before
            simply returning false. (Use 0 for no maximum.)
        :type max_models: int
         N/A N/A model_builder None N/A N/A N/A isinstance model_builder Mace N/A N/A model_builder N/A Mace max_models N/A N/A N/A BaseModelBuilderCommand __init__ self model_builder goal assumptions N/A valuation N/A N/A mbc N/A N/A N/A N/A N/A mbc model valuation N/A property _convert2val N/A N/A self valuation_str N/A N/A N/A 
        Transform the output file into an NLTK-style Valuation.

        :return: A model if one is generated; None otherwise.
        :rtype: sem.Valuation
         N/A valuation_standard_format N/A N/A self _transform_output valuation_str standard N/A val N/A N/A line N/A N/A valuation_standard_format splitlines False N/A N/A l N/A N/A line strip N/A N/A N/A l startswith interpretation N/A N/A num_entities N/A int N/A N/A N/A l N/A N/A N/A N/A l index ( 1 N/A N/A l index , strip N/A N/A N/A N/A N/A l startswith function N/A N/A N/A l find _ -1 N/A N/A name N/A N/A N/A l N/A N/A N/A N/A l index ( 1 N/A N/A l index , strip N/A N/A is_indvar name N/A N/A name N/A N/A name upper N/A value N/A int N/A N/A N/A l N/A N/A N/A N/A l index [ 1 N/A N/A l index ] strip N/A N/A N/A val append N/A name N/A N/A MaceCommand _make_model_var value N/A N/A N/A N/A l startswith relation N/A N/A l N/A l N/A N/A N/A N/A l index ( 1 N/A N/A ( l N/A N/A name N/A N/A N/A l N/A N/A N/A l index ( strip N/A values N/A N/A int N/A N/A v strip N/A v N/A N/A N/A l N/A N/A N/A N/A l index [ 1 N/A N/A l index ] split , N/A N/A N/A val append N/A name N/A N/A MaceCommand _make_relation_set num_entities values N/A N/A name N/A N/A N/A l N/A N/A N/A l index , strip N/A value N/A int N/A N/A N/A l N/A N/A N/A N/A l index [ 1 N/A N/A l index ] strip N/A N/A N/A val append N/A name N/A value 1 N/A N/A Valuation val N/A _make_relation_set N/A N/A num_entities values N/A N/A N/A 
        Convert a Mace4-style relation table into a dictionary.

        :param num_entities: the number of entities in the model; determines the row length in the table.
        :type num_entities: int
        :param values: a list of 1's and 0's that represent whether a relation holds in a Mace4 model.
        :type values: list of int
         N/A r N/A set N/A position N/A pos N/A N/A pos v N/A enumerate values N/A v 1 N/A N/A N/A N/A r add N/A tuple N/A N/A MaceCommand _make_relation_tuple position values num_entities N/A r N/A staticmethod _make_relation_tuple N/A N/A position values num_entities N/A N/A N/A N/A N/A len values 1 N/A N/A N/A N/A N/A sublist_size N/A N/A len values num_entities N/A sublist_start N/A position sublist_size N/A sublist_position N/A int N/A position sublist_size N/A sublist N/A values N/A N/A sublist_start sublist_size N/A N/A sublist_start 1 sublist_size N/A N/A N/A N/A N/A MaceCommand _make_model_var sublist_start N/A N/A MaceCommand _make_relation_tuple sublist_position sublist num_entities N/A staticmethod _make_model_var N/A N/A value N/A N/A N/A 
        Pick an alphabetic character as identifier for an entity in the model.

        :param value: where to index into the list of characters
        :type value: int
         N/A letter N/A N/A a b c d e f g h i j k l m n o p q r s t u v w x y z N/A value N/A num N/A value 26 N/A N/A N/A num 0 N/A letter N/A str num letter N/A staticmethod _decorate_model N/A N/A self valuation_str format N/A N/A N/A 
        Print out a Mace4 model using any Mace4 ``interpformat`` format.
        See http://www.cs.unm.edu/~mccune/mace4/manual/ for details.

        :param valuation_str: str with the model builder's output
        :param format: str indicating the format for displaying
        models. Defaults to 'standard' format.
        :return: str
         N/A N/A format N/A N/A valuation_str N/A N/A N/A format valuation N/A N/A N/A N/A self _convert2val valuation_str N/A N/A N/A N/A self _transform_output valuation_str format N/A _transform_output N/A N/A self valuation_str format N/A N/A N/A 
        Transform the output file into any Mace4 ``interpformat`` format.

        :param format: Output format for displaying models.
        :type format: str
         N/A N/A format N/A standard standard2 portable tabular raw cooked xml tex N/A N/A N/A N/A N/A self _call_interpformat valuation_str N/A format N/A 0 N/A N/A N/A LookupError The specified format does not exist N/A _call_interpformat N/A N/A self input_str args verbose N/A N/A False N/A N/A 
        Call the ``interpformat`` binary with the given input.

        :param input_str: A string whose contents are used as stdin.
        :param args: A list of command-line arguments.
        :return: A tuple (stdout, returncode)
        :see: ``config_prover9``
         N/A N/A N/A self _interpformat_bin None N/A N/A N/A self _interpformat_bin N/A N/A N/A self _modelbuilder _find_binary interpformat verbose N/A N/A N/A N/A self _modelbuilder _call input_str N/A self _interpformat_bin args verbose N/A N/A Mace N/A Prover9Parent ModelBuilder N/A N/A _mace4_bin None __init__ N/A N/A self end_size N/A 500 N/A N/A N/A self _end_size end_size N/A The maximum model size that Mace will try before
           simply returning false. (Use -1 for no maximum.) N/A _build_model N/A N/A self goal assumptions verbose N/A None None False N/A N/A 
        Use Mace4 to build a first order model.

        :return: ``True`` if a model was found (i.e. Mace returns value of 0),
        else ``False``
         N/A N/A assumptions N/A N/A assumptions N/A N/A N/A stdout returncode N/A N/A self _call_mace4 N/A N/A self prover9_input goal assumptions verbose verbose N/A N/A N/A returncode 0 stdout N/A _call_mace4 N/A N/A self input_str args verbose N/A N/A False N/A N/A 
        Call the ``mace4`` binary with the given input.

        :param input_str: A string whose contents are used as stdin.
        :param args: A list of command-line arguments.
        :return: A tuple (stdout, returncode)
        :see: ``config_prover9``
         N/A N/A N/A self _mace4_bin None N/A N/A N/A self _mace4_bin N/A N/A self _find_binary mace4 verbose N/A updated_input_str N/A N/A N/A self _end_size 0 N/A N/A updated_input_str N/A assign(end_size, %d).

 N/A self _end_size N/A updated_input_str input_str N/A N/A N/A self _call updated_input_str N/A self _mace4_bin args verbose N/A N/A spacer N/A N/A num N/A 30 N/A N/A N/A print N/A - num N/A decode_result N/A N/A found N/A N/A N/A 
    Decode the result of model_found()

    :param found: The output of model_found()
    :type found: bool
     N/A N/A N/A True False None Countermodel found No countermodel found None N/A found N/A test_model_found N/A N/A arguments N/A N/A N/A 
    Try some proofs and exhibit the results.
     N/A N/A goal assumptions arguments N/A N/A g N/A N/A Expression fromstring goal N/A alist N/A N/A N/A lp parse a N/A a assumptions N/A m N/A MaceCommand g assumptions alist max_models 50 N/A found N/A N/A m build_model N/A a alist N/A N/A N/A print N/A    %s a N/A N/A print N/A |- %s: %s
 N/A g N/A decode_result found N/A test_build_model N/A N/A arguments N/A N/A N/A 
    Try to build a ``nltk.sem.Valuation``.
     N/A g N/A N/A Expression fromstring all x.man(x) N/A alist N/A N/A N/A Expression fromstring a N/A a N/A man(John) man(Socrates) man(Bill) some x.(-(x = John) & man(x) & sees(John,x)) some x.(-(x = Bill) & man(x)) all x.some y.(man(x) -> gives(Socrates,x,y)) N/A m N/A MaceCommand g assumptions alist N/A N/A N/A m build_model N/A N/A spacer N/A N/A print Assumptions and Goal N/A N/A spacer N/A a alist N/A N/A N/A print N/A    %s a N/A N/A print N/A |- %s: %s
 N/A g N/A decode_result N/A N/A m build_model N/A N/A spacer N/A N/A print Valuation N/A N/A spacer N/A N/A print N/A m valuation N/A test_transform_output N/A N/A argument_pair N/A N/A N/A 
    Transform the model into various Mace4 ``interpformat`` formats.
     N/A g N/A N/A Expression fromstring N/A argument_pair N/A 0 N/A alist N/A N/A N/A lp parse a N/A a N/A argument_pair N/A 1 N/A m N/A MaceCommand g assumptions alist N/A N/A N/A m build_model N/A a alist N/A N/A N/A print N/A    %s a N/A N/A print N/A |- %s: %s
 N/A g N/A N/A m build_model N/A format N/A standard portable xml cooked N/A N/A N/A spacer N/A N/A print N/A Using '%s' format format N/A N/A spacer N/A N/A print N/A N/A m model format format N/A test_make_relation_set N/A N/A N/A N/A N/A N/A print N/A N/A N/A MaceCommand _make_relation_set num_entities 3 values N/A 1 0 1 N/A set N/A N/A c N/A a N/A N/A print N/A N/A N/A MaceCommand _make_relation_set num_entities 3 values N/A 0 0 0 0 0 0 1 0 0 N/A set N/A N/A c a N/A N/A print N/A N/A N/A MaceCommand _make_relation_set num_entities 2 values N/A 0 0 1 0 0 0 1 0 N/A set N/A N/A a b a N/A b b a N/A N/A arguments N/A N/A mortal(Socrates) N/A all x.(man(x) -> mortal(x)) man(Socrates) N/A (not mortal(Socrates)) N/A all x.(man(x) -> mortal(x)) man(Socrates) demo N/A N/A N/A N/A N/A N/A test_model_found arguments N/A N/A test_build_model arguments N/A N/A test_transform_output N/A arguments N/A 1 N/A N/A N/A __name__ __main__ N/A N/A N/A demo