Module Expr Str ImportFrom alias alias ImportFrom alias alias alias alias ImportFrom alias ImportFrom alias FunctionDef arguments args NameParam defaults body Expr Str If BoolOpOr CompareIs NameLoad NameLoad CompareIs NameLoad NameLoad body Return NameLoad TryExcept body If AttributeLoad NameLoad attr body Return NameLoad If AttributeLoad NameLoad attr body Return Call NameLoad SubscriptLoad AttributeLoad NameLoad attr Index Num orelse Raise NameLoad handlers ExceptHandler type TupleLoad NameLoad NameLoad body Raise Call NameLoad Str decorator_list FunctionDef arguments args NameParam NameParam NameParam defaults Str NameLoad body Expr Str Assign NameStore Call NameLoad NameLoad If CompareEq NameLoad Str body ImportFrom alias Return Call NameLoad NameLoad orelse If CompareEq NameLoad Str body ImportFrom alias Return Call NameLoad NameLoad NameLoad Raise NameLoad decorator_list FunctionDef arguments args NameParam defaults body Expr Str Return UnaryOpNot Call NameLoad Call NameLoad NameLoad decorator_list FunctionDef arguments args NameParam NameParam NameParam defaults Dict NameLoad body Expr Str ImportFrom alias ImportFrom alias Assign NameStore TupleLoad NameLoad NameLoad FunctionDef arguments args NameParam defaults body If BoolOpOr Call NameLoad NameLoad NameLoad CompareIn NameLoad NameLoad body Return NameLoad If UnaryOpNot Call NameLoad NameLoad NameLoad body Return NameLoad Return Call NameLoad GeneratorExp Call NameLoad NameLoad comprehension NameStore AttributeLoad NameLoad attr decorator_list If CompareIn NameLoad NameLoad body Return NameLoad Assign NameStore Call NameLoad NameLoad If UnaryOpNot Call NameLoad NameLoad body Raise Call NameLoad BinOpMod Str NameLoad Assign NameStore Call NameLoad GeneratorExp TupleLoad NameLoad NameLoad comprehension TupleStore NameStore NameStore Call AttributeLoad NameLoad attr CompareIn NameLoad NameLoad Assign NameStore Call AttributeLoad NameLoad attr NameLoad If CompareIn NameLoad NameLoad body Return Call NameLoad NameLoad If NameLoad body Assign NameStore Call NameLoad GeneratorExp TupleLoad NameLoad NameLoad comprehension NameStore Call AttributeLoad NameLoad attr If Call NameLoad NameLoad NameLoad body If Call NameLoad NameLoad body Return NameLoad orelse If UnaryOpNot Call NameLoad NameLoad body Return NameLoad Return NameLoad decorator_list FunctionDef arguments args NameParam NameParam defaults Dict body Expr Str Assign NameStore Call NameLoad NameLoad Expr Call AttributeLoad NameLoad attr Call NameLoad NameLoad Return UnaryOpNot Call NameLoad Call NameLoad NameLoad decorator_list ClassDef bases NameLoad body Expr Str FunctionDef arguments args NameParam NameParam defaults NameLoad body Assign AttributeStore NameLoad attr Call NameLoad If NameLoad body Expr Call AttributeLoad NameLoad attr NameLoad decorator_list FunctionDef arguments args NameParam NameParam defaults body Raise NameLoad decorator_list FunctionDef arguments args NameParam NameParam defaults body Raise NameLoad decorator_list FunctionDef arguments args NameParam NameParam defaults body Raise NameLoad decorator_list FunctionDef arguments args NameParam defaults body Return Call NameLoad Call NameLoad AttributeLoad NameLoad attr decorator_list NameLoad decorator_list ClassDef bases NameLoad body Expr Str FunctionDef arguments args NameParam NameParam defaults body Expr Str For NameStore Call NameLoad Call NameLoad NameLoad body Expr Call AttributeLoad AttributeLoad NameLoad attr attr NameLoad decorator_list FunctionDef arguments args NameParam NameParam defaults body Expr Str Return Call NameLoad NameLoad AttributeLoad NameLoad attr decorator_list FunctionDef arguments args NameParam NameParam defaults body Expr Str For NameStore Call NameLoad Call NameLoad NameLoad body Expr Call AttributeLoad AttributeLoad NameLoad attr attr NameLoad decorator_list decorator_list
N/A N/A Inference in propositional logic __future__ print_function division sympy.logic.boolalg And Not conjuncts to_cnf sympy.core.compatibility ordered sympy.core.sympify sympify literal_symbol N/A N/A literal N/A N/A N/A 
    The symbol in this literal (without the negation).

    Examples
    ========

    >>> from sympy.abc import A
    >>> from sympy.logic.inference import literal_symbol
    >>> literal_symbol(A)
    A
    >>> literal_symbol(~A)
    A

     N/A N/A N/A literal True N/A literal False N/A N/A literal N/A N/A N/A N/A literal is_Symbol N/A N/A literal N/A N/A literal is_Not N/A N/A N/A literal_symbol N/A N/A literal args N/A 0 N/A N/A ValueError N/A N/A N/A N/A AttributeError ValueError N/A N/A N/A ValueError Argument must be a boolean literal. N/A satisfiable N/A N/A expr algorithm all_models N/A dpll2 False N/A N/A 
    Check satisfiability of a propositional sentence.
    Returns a model when it succeeds.
    Returns {true: true} for trivially true expressions.

    On setting all_models to True, if given expr is satisfiable then
    returns a generator of models. However, if expr is unsatisfiable
    then returns a generator containing the single element False.

    Examples
    ========

    >>> from sympy.abc import A, B
    >>> from sympy.logic.inference import satisfiable
    >>> satisfiable(A & ~B)
    {A: True, B: False}
    >>> satisfiable(A & ~A)
    False
    >>> satisfiable(True)
    {True: True}
    >>> next(satisfiable(A & ~A, all_models=True))
    False
    >>> models = satisfiable((A >> B) & B, all_models=True)
    >>> next(models)
    {A: False, B: True}
    >>> next(models)
    {A: True, B: True}
    >>> def use_models(models):
    ...     for model in models:
    ...         if model:
    ...             # Do something with the model.
    ...             print(model)
    ...         else:
    ...             # Given expr is unsatisfiable.
    ...             print("UNSAT")
    >>> use_models(satisfiable(A >> ~A, all_models=True))
    {A: False}
    >>> use_models(satisfiable(A ^ A, all_models=True))
    UNSAT

     N/A expr N/A to_cnf expr N/A N/A algorithm dpll N/A sympy.logic.algorithms.dpll dpll_satisfiable N/A N/A dpll_satisfiable expr N/A N/A N/A algorithm dpll2 N/A sympy.logic.algorithms.dpll2 dpll_satisfiable N/A N/A dpll_satisfiable expr all_models N/A NotImplementedError N/A valid N/A N/A expr N/A N/A N/A 
    Check validity of a propositional sentence.
    A valid propositional sentence is True under every assignment.

    Examples
    ========

    >>> from sympy.abc import A, B
    >>> from sympy.logic.inference import valid
    >>> valid(A | ~A)
    True
    >>> valid(A | B)
    False

    References
    ==========

    .. [1] http://en.wikipedia.org/wiki/Validity

     N/A N/A N/A satisfiable N/A Not expr N/A pl_true N/A N/A expr model deep N/A N/A False N/A N/A 
    Returns whether the given assignment is a model or not.

    If the assignment does not specify the value for every proposition,
    this may return None to indicate 'not obvious'.

    Parameters
    ==========

    model : dict, optional, default: {}
        Mapping of symbols to boolean values to indicate assignment.
    deep: boolean, optional, default: False
        Gives the value of the expression under partial assignments
        correctly. May still return None to indicate 'not obvious'.


    Examples
    ========

    >>> from sympy.abc import A, B, C
    >>> from sympy.logic.inference import pl_true
    >>> pl_true( A & B, {A: True, B: True})
    True
    >>> pl_true(A & B, {A: False})
    False
    >>> pl_true(A & B, {A: True})
    >>> pl_true(A & B, {A: True}, deep=True)
    >>> pl_true(A >> (B >> A))
    >>> pl_true(A >> (B >> A), deep=True)
    True
    >>> pl_true(A & ~A)
    >>> pl_true(A & ~A, deep=True)
    False
    >>> pl_true(A & B & (~A | ~B), {A: True})
    >>> pl_true(A & B & (~A | ~B), {A: True}, deep=True)
    False
     sympy.core.symbol Symbol sympy.logic.boolalg BooleanFunction N/A boolean N/A True False _validate N/A N/A expr N/A N/A N/A N/A N/A isinstance expr Symbol N/A expr boolean N/A N/A True N/A N/A N/A isinstance expr BooleanFunction N/A N/A False N/A N/A all N/A N/A _validate arg N/A arg N/A expr args N/A N/A N/A expr boolean N/A N/A expr N/A expr N/A sympify expr N/A N/A N/A _validate expr N/A N/A N/A ValueError N/A %s is not a valid boolean expression expr N/A model N/A dict N/A N/A k v N/A N/A k v N/A N/A model items N/A v boolean N/A result N/A N/A expr subs model N/A N/A result boolean N/A N/A N/A bool result N/A deep N/A N/A model N/A dict N/A N/A k True N/A k N/A N/A result atoms N/A N/A pl_true result model N/A N/A N/A valid result N/A N/A True N/A N/A N/A N/A satisfiable result N/A N/A False N/A None N/A entails N/A N/A expr formula_set N/A N/A N/A N/A 
    Check whether the given expr_set entail an expr.
    If formula_set is empty then it returns the validity of expr.

    Examples
    ========

    >>> from sympy.abc import A, B, C
    >>> from sympy.logic.inference import entails
    >>> entails(A, [A >> B, B >> C])
    False
    >>> entails(C, [A >> B, B >> C, A])
    True
    >>> entails(A >> B)
    False
    >>> entails(A >> (B >> A))
    True

    References
    ==========

    .. [1] http://en.wikipedia.org/wiki/Logical_consequence

     N/A formula_set N/A list formula_set N/A N/A N/A formula_set append N/A Not expr N/A N/A N/A satisfiable N/A And formula_set N/A KB N/A object N/A N/A Base class for all knowledge bases __init__ N/A N/A self sentence N/A None N/A N/A N/A self clauses_ N/A set N/A sentence N/A N/A N/A N/A self tell sentence N/A tell N/A N/A self sentence N/A N/A N/A NotImplementedError N/A ask N/A N/A self query N/A N/A N/A NotImplementedError N/A retract N/A N/A self sentence N/A N/A N/A NotImplementedError N/A clauses N/A N/A self N/A N/A N/A N/A list N/A ordered N/A self clauses_ N/A property N/A PropKB N/A KB N/A N/A A KB for Propositional Logic.  Inefficient, with no indexing. tell N/A N/A self sentence N/A N/A N/A Add the sentence's clauses to the KB

        Examples
        ========

        >>> from sympy.logic.inference import PropKB
        >>> from sympy.abc import x, y
        >>> l = PropKB()
        >>> l.clauses
        []

        >>> l.tell(x | y)
        >>> l.clauses
        [Or(x, y)]

        >>> l.tell(y)
        >>> l.clauses
        [y, Or(x, y)]
         N/A c N/A conjuncts N/A to_cnf sentence N/A N/A N/A N/A N/A self clauses_ add c N/A ask N/A N/A self query N/A N/A N/A Checks if the query is true given the set of clauses.

        Examples
        ========

        >>> from sympy.logic.inference import PropKB
        >>> from sympy.abc import x, y
        >>> l = PropKB()
        >>> l.tell(x & ~y)
        >>> l.ask(x)
        True
        >>> l.ask(y)
        False
         N/A N/A entails query N/A self clauses_ N/A retract N/A N/A self sentence N/A N/A N/A Remove the sentence's clauses from the KB

        Examples
        ========

        >>> from sympy.logic.inference import PropKB
        >>> from sympy.abc import x, y
        >>> l = PropKB()
        >>> l.clauses
        []

        >>> l.tell(x | y)
        >>> l.clauses
        [Or(x, y)]

        >>> l.retract(x | y)
        >>> l.clauses
        []
         N/A c N/A conjuncts N/A to_cnf sentence N/A N/A N/A N/A N/A self clauses_ discard c N/A N/A