Repository: sympy/sympy
Pull request: feat(assumptions): reorganize facts for new assumptions
<!-- Your title above should be a short description of what
was changed. Do not include the issue number in the title. -->

#### References to other Issues or PRs
<!-- If this pull request fixes an issue, write "Fixes #NNNN" in that exact
format, e.g. "Fixes #1234" (see
https://tinyurl.com/auto-closing for more information). Also, please
write a comment on that issue linking back to this pull request once it is
open. -->

Fixes #21228

#### Brief description of what is fixed or changed

* `Q.positive_infinite()` and `Q.negative_infinite()` predicates are introduced.
* `Q.extended_positive()`, `Q.extended_negative()`, `Q.extended_nonzero()`, `Q.extended_nonpositive()`, and `Q.extended_nonnegative()` predicates are introduced.
* `Q.positive()` and `Q.negative()` now correctly implies the argument being finite.
* Incorrect results from `Q.hermitian()` and `Q.antihermitian()` are fixed.

* In order to reduce the complexity of sat solver, some predicates are now decomposed into a combination of primitive predicates.
* Facts are now defined in `assumptions/facts.py`, instead of in `assumptions/ask.py`.

#### Other comments
Benchmark showed no slowdown.

#### Release Notes

<!-- Write the release notes for this release below between the BEGIN and END
statements. The basic format is a bulleted list with the name of the subpackage
and the release note for this PR. For example:

* solvers
  * Added a new solver for logarithmic equations.

* functions
  * Fixed a bug with log of integers.

or if no release note(s) should be included use:

NO ENTRY

See https://github.com/sympy/sympy/wiki/Writing-Release-Notes for more
information on how to write release notes. The bot will check your release
notes automatically to see if they are formatted correctly. -->

<!-- BEGIN RELEASE NOTES -->
* assumptions
  * `Q.positive_infinite()` and `Q.negative_infinite()` predicates are introduced.
  * `Q.extended_positive()`, `Q.extended_negative()`, `Q.extended_nonzero()`, `Q.extended_nonpositive()`, and `Q.extended_nonnegative()` predicates are introduced.
  * `Q.positive()` and `Q.negative()` now correctly implies the argument being finite.
  * Incorrect results from `Q.hermitian()` and `Q.antihermitian()` are fixed.
<!-- END RELEASE NOTES -->


Problem statement:
Incorrect assumption for is_hermitian
An object being antihermitian implies it being not hermitian in new assumption system. (and vice versa)

```python
>>> ask(Q.hermitian(x), Q.antihermitian(x))
False
```

But in old assumptions system, it does not.

```python
>>> x = Symbol('x', antihermitian=True)
>>> print(x.is_hermitian)
None
```

Is this an error of core/assumptions module?

Hints from issue discussion:
A matrix or operator can be neither hermitian nor antihermitian so that's a bug in the new assumptions.

I don't think that hermitian/antihermitian should be part of the old assumptions.
It is true that an operator being not hermitian does not mean that it is antihermitian.   But doesn't an operator ***being hermitian*** means that it is ***not antihermitian***?
The zero operator is an operator which is hermitian and antihermitian, and it is the only such operator (unless the characteristic of the ground field is 2).
Hence this is an error and `None` would be the correct output. Maybe there should be a `nonzero` assumption for operators.
It would also make sense to introduce `positive` and `negative` assumptions for operators etc.
Thanks. Didn't notice that!

Commit message: feat(assumptions) : reorganize new assumption fact

Fix test_known_facts_consistent()

Patch to review:
diff --git a/bin/ask_update.py b/bin/ask_update.py
index 97d0485b3682..345d0e4759e8 100755
--- a/bin/ask_update.py
+++ b/bin/ask_update.py
@@ -21,7 +21,7 @@
 if os.path.isdir(sympy_dir):
     sys.path.insert(0, sympy_top)
 
-from sympy.assumptions.ask import (compute_known_facts,
+from sympy.assumptions.facts import (compute_known_facts,
         get_known_facts, get_known_facts_keys)
 
 with open('sympy/assumptions/ask_generated.py', 'w') as f:
diff --git a/sympy/assumptions/ask.py b/sympy/assumptions/ask.py
index 8e2f85ec2ba1..2069eba52327 100644
--- a/sympy/assumptions/ask.py
+++ b/sympy/assumptions/ask.py
@@ -4,10 +4,9 @@
         AppliedPredicate)
 from sympy.assumptions.cnf import CNF, EncodedCNF, Literal
 from sympy.core import sympify
-from sympy.core.cache import cacheit
 from sympy.core.kind import BooleanKind
 from sympy.core.relational import Eq, Ne, Gt, Lt, Ge, Le
-from sympy.logic.boolalg import (to_cnf, And, Not, Implies, Equivalent)
+from sympy.logic.boolalg import Not
 from sympy.logic.inference import satisfiable
 from sympy.utilities.decorator import memoize_property
 from sympy.utilities.exceptions import SymPyDeprecationWarning
@@ -91,9 +90,19 @@ def finite(self):
 
     @memoize_property
     def infinite(self):
-        from .predicates.calculus import InfinitePredicate
+        from .handlers.calculus import InfinitePredicate
         return InfinitePredicate()
 
+    @memoize_property
+    def positive_infinite(self):
+        from .handlers.calculus import PositiveInfinitePredicate
+        return PositiveInfinitePredicate()
+
+    @memoize_property
+    def negative_infinite(self):
+        from .handlers.calculus import NegativeInfinitePredicate
+        return NegativeInfinitePredicate()
+
     @memoize_property
     def positive(self):
         from .handlers.order import PositivePredicate
@@ -109,6 +118,16 @@ def zero(self):
         from .handlers.order import ZeroPredicate
         return ZeroPredicate()
 
+    @memoize_property
+    def extended_positive(self):
+        from .handlers.order import ExtendedPositivePredicate
+        return ExtendedPositivePredicate()
+
+    @memoize_property
+    def extended_negative(self):
+        from .handlers.order import ExtendedNegativePredicate
+        return ExtendedNegativePredicate()
+
     @memoize_property
     def nonzero(self):
         from .handlers.order import NonZeroPredicate
@@ -124,6 +143,21 @@ def nonnegative(self):
         from .handlers.order import NonNegativePredicate
         return NonNegativePredicate()
 
+    @memoize_property
+    def extended_nonzero(self):
+        from .handlers.order import ExtendedNonZeroPredicate
+        return ExtendedNonZeroPredicate()
+
+    @memoize_property
+    def extended_nonpositive(self):
+        from .handlers.order import ExtendedNonPositivePredicate
+        return ExtendedNonPositivePredicate()
+
+    @memoize_property
+    def extended_nonnegative(self):
+        from .handlers.order import ExtendedNonNegativePredicate
+        return ExtendedNonNegativePredicate()
+
     @memoize_property
     def even(self):
         from .handlers.ntheory import EvenPredicate
@@ -407,16 +441,14 @@ def ask(proposition, assumptions=True, context=global_assumptions):
         key, args = Q.is_true, (proposition,)
 
     # convert local and global assumptions to CNF
-    assump = CNF.from_prop(assumptions)
-    assump.extend(context)
+    assump_cnf = CNF.from_prop(assumptions)
+    assump_cnf.extend(context)
 
     # extract the relevant facts from assumptions with respect to args
-    local_facts = _extract_all_facts(assump, args)
-
-    known_facts_cnf = get_all_known_facts()
-    known_facts_dict = get_known_facts_dict()
+    local_facts = _extract_all_facts(assump_cnf, args)
 
     # convert default facts and assumed facts to encoded CNF
+    known_facts_cnf = get_all_known_facts()
     enc_cnf = EncodedCNF()
     enc_cnf.from_cnf(CNF(known_facts_cnf))
     enc_cnf.add_from_cnf(local_facts)
@@ -425,10 +457,11 @@ def ask(proposition, assumptions=True, context=global_assumptions):
     if local_facts.clauses and satisfiable(enc_cnf) is False:
         raise ValueError("inconsistent assumptions %s" % assumptions)
 
+    known_facts_dict = get_known_facts_dict()
     if local_facts.clauses:
 
         # quick exit if the prerequisite of proposition is not true
-        # e.g. proposition = Q.odd(x), assumptions = ~Q.integer(x)
+        # e.g. proposition = Q.zero(x), assumptions = ~Q.even(x)
         if len(local_facts.clauses) == 1:
             cl, = local_facts.clauses
             if len(cl) == 1:
@@ -444,7 +477,7 @@ def ask(proposition, assumptions=True, context=global_assumptions):
                     pass
                 elif key in fdict:
                     # quick exit if proposition is directly satisfied by assumption
-                    # e.g. proposition = Q.integer(x), assumptions = Q.odd(x)
+                    # e.g. proposition = Q.even(x), assumptions = Q.zero(x)
                     return True
                 elif Not(key) in fdict:
                     # quick exit if proposition is directly rejected by assumption
@@ -457,23 +490,12 @@ def ask(proposition, assumptions=True, context=global_assumptions):
     res = key(*args)._eval_ask(assumptions)
     if res is not None:
         return bool(res)
+
     # using satask (still costly)
     res = satask(proposition, assumptions=assumptions, context=context)
     return res
 
 
-def ask_full_inference(proposition, assumptions, known_facts_cnf):
-    """
-    Method for inferring properties about objects.
-
-    """
-    if not satisfiable(And(known_facts_cnf, assumptions, proposition)):
-        return False
-    if not satisfiable(And(known_facts_cnf, assumptions, Not(proposition))):
-        return True
-    return None
-
-
 def register_handler(key, handler):
     """
     Register a handler in the ask system. key must be a string and handler a
@@ -517,148 +539,5 @@ def remove_handler(key, handler):
     getattr(Q, key).remove_handler(handler)
 
 
-def single_fact_lookup(known_facts_keys, known_facts_cnf):
-    # Compute the quick lookup for single facts
-    mapping = {}
-    for key in known_facts_keys:
-        mapping[key] = {key}
-        for other_key in known_facts_keys:
-            if other_key != key:
-                if ask_full_inference(other_key, key, known_facts_cnf):
-                    mapping[key].add(other_key)
-    return mapping
-
-
-def compute_known_facts(known_facts, known_facts_keys):
-    """Compute the various forms of knowledge compilation used by the
-    assumptions system.
-
-    Explanation
-    ===========
-
-    This function is typically applied to the results of the ``get_known_facts``
-    and ``get_known_facts_keys`` functions defined at the bottom of
-    this file.
-    """
-    from textwrap import dedent, wrap
-
-    fact_string = dedent('''\
-    """
-    The contents of this file are the return value of
-    ``sympy.assumptions.ask.compute_known_facts``.
-
-    Do NOT manually edit this file.
-    Instead, run ./bin/ask_update.py.
-    """
-
-    from sympy.core.cache import cacheit
-    from sympy.logic.boolalg import And
-    from sympy.assumptions.cnf import Literal
-    from sympy.assumptions.ask import Q
-
-    # -{ Known facts as a set }-
-    @cacheit
-    def get_all_known_facts():
-        return {
-            %s
-        }
-
-    # -{ Known facts in Conjunctive Normal Form }-
-    @cacheit
-    def get_known_facts_cnf():
-        return And(
-            %s
-        )
-
-    # -{ Known facts in compressed sets }-
-    @cacheit
-    def get_known_facts_dict():
-        return {
-            %s
-        }
-    ''')
-    # Compute the known facts in CNF form for logical inference
-    LINE = ",\n        "
-    HANG = ' '*8
-    cnf = to_cnf(known_facts)
-    cnf_ = CNF.to_CNF(known_facts)
-    c = LINE.join([str(a) for a in cnf.args])
-
-    p = LINE.join(sorted(['frozenset((' + ', '.join(str(lit) for lit in sorted(clause, key=str)) +'))' for clause in cnf_.clauses]))
-    mapping = single_fact_lookup(known_facts_keys, cnf)
-    items = sorted(mapping.items(), key=str)
-    keys = [str(i[0]) for i in items]
-    values = ['set(%s)' % sorted(i[1], key=str) for i in items]
-    m = LINE.join(['\n'.join(
-        wrap("{}: {}".format(k, v),
-            subsequent_indent=HANG,
-            break_long_words=False))
-        for k, v in zip(keys, values)]) + ','
-    return fact_string % (p, c, m)
-
-@cacheit
-def get_known_facts_keys():
-    return [
-        getattr(Q, attr)
-        for attr in Q.__class__.__dict__
-        if not attr.startswith('__')]
-
-@cacheit
-def get_known_facts():
-    return And(
-        Implies(Q.infinite, ~Q.finite),
-        Implies(Q.real, Q.complex),
-        Implies(Q.real, Q.hermitian),
-        Equivalent(Q.extended_real, Q.real | Q.infinite),
-        Equivalent(Q.even | Q.odd, Q.integer),
-        Implies(Q.even, ~Q.odd),
-        Implies(Q.prime, Q.integer & Q.positive & ~Q.composite),
-        Implies(Q.integer, Q.rational),
-        Implies(Q.rational, Q.algebraic),
-        Implies(Q.algebraic, Q.complex),
-        Implies(Q.algebraic, Q.finite),
-        Equivalent(Q.transcendental | Q.algebraic, Q.complex & Q.finite),
-        Implies(Q.transcendental, ~Q.algebraic),
-        Implies(Q.transcendental, Q.finite),
-        Implies(Q.imaginary, Q.complex & ~Q.real),
-        Implies(Q.imaginary, Q.antihermitian),
-        Implies(Q.antihermitian, ~Q.hermitian),
-        Equivalent(Q.irrational | Q.rational, Q.real & Q.finite),
-        Implies(Q.irrational, ~Q.rational),
-        Implies(Q.zero, Q.even),
-
-        Equivalent(Q.real, Q.negative | Q.zero | Q.positive),
-        Implies(Q.zero, ~Q.negative & ~Q.positive),
-        Implies(Q.negative, ~Q.positive),
-        Equivalent(Q.nonnegative, Q.zero | Q.positive),
-        Equivalent(Q.nonpositive, Q.zero | Q.negative),
-        Equivalent(Q.nonzero, Q.negative | Q.positive),
-
-        Implies(Q.orthogonal, Q.positive_definite),
-        Implies(Q.orthogonal, Q.unitary),
-        Implies(Q.unitary & Q.real, Q.orthogonal),
-        Implies(Q.unitary, Q.normal),
-        Implies(Q.unitary, Q.invertible),
-        Implies(Q.normal, Q.square),
-        Implies(Q.diagonal, Q.normal),
-        Implies(Q.positive_definite, Q.invertible),
-        Implies(Q.diagonal, Q.upper_triangular),
-        Implies(Q.diagonal, Q.lower_triangular),
-        Implies(Q.lower_triangular, Q.triangular),
-        Implies(Q.upper_triangular, Q.triangular),
-        Implies(Q.triangular, Q.upper_triangular | Q.lower_triangular),
-        Implies(Q.upper_triangular & Q.lower_triangular, Q.diagonal),
-        Implies(Q.diagonal, Q.symmetric),
-        Implies(Q.unit_triangular, Q.triangular),
-        Implies(Q.invertible, Q.fullrank),
-        Implies(Q.invertible, Q.square),
-        Implies(Q.symmetric, Q.square),
-        Implies(Q.fullrank & Q.square, Q.invertible),
-        Equivalent(Q.invertible, ~Q.singular),
-        Implies(Q.integer_elements, Q.real_elements),
-        Implies(Q.real_elements, Q.complex_elements),
-    )
-
-
 from sympy.assumptions.ask_generated import (
     get_known_facts_dict, get_all_known_facts)
diff --git a/sympy/assumptions/ask_generated.py b/sympy/assumptions/ask_generated.py
index 1eb45b4cd9b2..536757a223b8 100644
--- a/sympy/assumptions/ask_generated.py
+++ b/sympy/assumptions/ask_generated.py
@@ -15,75 +15,68 @@
 @cacheit
 def get_all_known_facts():
     return {
-        frozenset((Literal(Q.algebraic, False), Literal(Q.complex, True), Literal(Q.finite, True), Literal(Q.transcendental, False))),
+        frozenset((Literal(Q.algebraic, False), Literal(Q.imaginary, True), Literal(Q.transcendental, False))),
+        frozenset((Literal(Q.algebraic, False), Literal(Q.negative, True), Literal(Q.transcendental, False))),
+        frozenset((Literal(Q.algebraic, False), Literal(Q.positive, True), Literal(Q.transcendental, False))),
         frozenset((Literal(Q.algebraic, False), Literal(Q.rational, True))),
-        frozenset((Literal(Q.algebraic, True), Literal(Q.complex, False))),
+        frozenset((Literal(Q.algebraic, False), Literal(Q.transcendental, False), Literal(Q.zero, True))),
         frozenset((Literal(Q.algebraic, True), Literal(Q.finite, False))),
         frozenset((Literal(Q.algebraic, True), Literal(Q.transcendental, True))),
+        frozenset((Literal(Q.antihermitian, False), Literal(Q.hermitian, False), Literal(Q.zero, True))),
         frozenset((Literal(Q.antihermitian, False), Literal(Q.imaginary, True))),
-        frozenset((Literal(Q.antihermitian, True), Literal(Q.hermitian, True))),
-        frozenset((Literal(Q.complex, False), Literal(Q.imaginary, True))),
-        frozenset((Literal(Q.complex, False), Literal(Q.real, True))),
-        frozenset((Literal(Q.complex, False), Literal(Q.transcendental, True))),
+        frozenset((Literal(Q.commutative, False), Literal(Q.finite, True))),
+        frozenset((Literal(Q.commutative, False), Literal(Q.infinite, True))),
         frozenset((Literal(Q.complex_elements, False), Literal(Q.real_elements, True))),
+        frozenset((Literal(Q.composite, False), Literal(Q.even, True), Literal(Q.positive, True), Literal(Q.prime, False))),
+        frozenset((Literal(Q.composite, True), Literal(Q.even, False), Literal(Q.odd, False))),
+        frozenset((Literal(Q.composite, True), Literal(Q.positive, False))),
         frozenset((Literal(Q.composite, True), Literal(Q.prime, True))),
         frozenset((Literal(Q.diagonal, False), Literal(Q.lower_triangular, True), Literal(Q.upper_triangular, True))),
         frozenset((Literal(Q.diagonal, True), Literal(Q.lower_triangular, False))),
         frozenset((Literal(Q.diagonal, True), Literal(Q.normal, False))),
         frozenset((Literal(Q.diagonal, True), Literal(Q.symmetric, False))),
         frozenset((Literal(Q.diagonal, True), Literal(Q.upper_triangular, False))),
-        frozenset((Literal(Q.even, False), Literal(Q.integer, True), Literal(Q.odd, False))),
+        frozenset((Literal(Q.even, False), Literal(Q.odd, False), Literal(Q.prime, True))),
         frozenset((Literal(Q.even, False), Literal(Q.zero, True))),
-        frozenset((Literal(Q.even, True), Literal(Q.integer, False))),
         frozenset((Literal(Q.even, True), Literal(Q.odd, True))),
-        frozenset((Literal(Q.extended_real, False), Literal(Q.infinite, True))),
-        frozenset((Literal(Q.extended_real, False), Literal(Q.real, True))),
-        frozenset((Literal(Q.extended_real, True), Literal(Q.infinite, False), Literal(Q.real, False))),
-        frozenset((Literal(Q.finite, False), Literal(Q.irrational, True))),
-        frozenset((Literal(Q.finite, False), Literal(Q.rational, True))),
+        frozenset((Literal(Q.even, True), Literal(Q.rational, False))),
         frozenset((Literal(Q.finite, False), Literal(Q.transcendental, True))),
         frozenset((Literal(Q.finite, True), Literal(Q.infinite, True))),
-        frozenset((Literal(Q.finite, True), Literal(Q.irrational, False), Literal(Q.rational, False), Literal(Q.real, True))),
         frozenset((Literal(Q.fullrank, False), Literal(Q.invertible, True))),
         frozenset((Literal(Q.fullrank, True), Literal(Q.invertible, False), Literal(Q.square, True))),
-        frozenset((Literal(Q.hermitian, False), Literal(Q.real, True))),
-        frozenset((Literal(Q.imaginary, True), Literal(Q.real, True))),
-        frozenset((Literal(Q.integer, False), Literal(Q.odd, True))),
-        frozenset((Literal(Q.integer, False), Literal(Q.prime, True))),
-        frozenset((Literal(Q.integer, True), Literal(Q.rational, False))),
+        frozenset((Literal(Q.hermitian, False), Literal(Q.negative, True))),
+        frozenset((Literal(Q.hermitian, False), Literal(Q.positive, True))),
+        frozenset((Literal(Q.hermitian, False), Literal(Q.zero, True))),
+        frozenset((Literal(Q.imaginary, True), Literal(Q.negative, True))),
+        frozenset((Literal(Q.imaginary, True), Literal(Q.positive, True))),
+        frozenset((Literal(Q.imaginary, True), Literal(Q.zero, True))),
+        frozenset((Literal(Q.infinite, False), Literal(Q.negative_infinite, True))),
+        frozenset((Literal(Q.infinite, False), Literal(Q.positive_infinite, True))),
         frozenset((Literal(Q.integer_elements, True), Literal(Q.real_elements, False))),
         frozenset((Literal(Q.invertible, False), Literal(Q.positive_definite, True))),
         frozenset((Literal(Q.invertible, False), Literal(Q.singular, False))),
         frozenset((Literal(Q.invertible, False), Literal(Q.unitary, True))),
         frozenset((Literal(Q.invertible, True), Literal(Q.singular, True))),
         frozenset((Literal(Q.invertible, True), Literal(Q.square, False))),
+        frozenset((Literal(Q.irrational, False), Literal(Q.negative, True), Literal(Q.rational, False))),
+        frozenset((Literal(Q.irrational, False), Literal(Q.positive, True), Literal(Q.rational, False))),
+        frozenset((Literal(Q.irrational, False), Literal(Q.rational, False), Literal(Q.zero, True))),
+        frozenset((Literal(Q.irrational, True), Literal(Q.negative, False), Literal(Q.positive, False), Literal(Q.zero, False))),
         frozenset((Literal(Q.irrational, True), Literal(Q.rational, True))),
-        frozenset((Literal(Q.irrational, True), Literal(Q.real, False))),
         frozenset((Literal(Q.lower_triangular, False), Literal(Q.triangular, True), Literal(Q.upper_triangular, False))),
         frozenset((Literal(Q.lower_triangular, True), Literal(Q.triangular, False))),
-        frozenset((Literal(Q.negative, False), Literal(Q.nonpositive, True), Literal(Q.zero, False))),
-        frozenset((Literal(Q.negative, False), Literal(Q.nonzero, True), Literal(Q.positive, False))),
-        frozenset((Literal(Q.negative, False), Literal(Q.positive, False), Literal(Q.real, True), Literal(Q.zero, False))),
-        frozenset((Literal(Q.negative, True), Literal(Q.nonpositive, False))),
-        frozenset((Literal(Q.negative, True), Literal(Q.nonzero, False))),
+        frozenset((Literal(Q.negative, False), Literal(Q.positive, False), Literal(Q.rational, True), Literal(Q.zero, False))),
         frozenset((Literal(Q.negative, True), Literal(Q.positive, True))),
-        frozenset((Literal(Q.negative, True), Literal(Q.real, False))),
         frozenset((Literal(Q.negative, True), Literal(Q.zero, True))),
-        frozenset((Literal(Q.nonnegative, False), Literal(Q.positive, True))),
-        frozenset((Literal(Q.nonnegative, False), Literal(Q.zero, True))),
-        frozenset((Literal(Q.nonnegative, True), Literal(Q.positive, False), Literal(Q.zero, False))),
-        frozenset((Literal(Q.nonpositive, False), Literal(Q.zero, True))),
-        frozenset((Literal(Q.nonzero, False), Literal(Q.positive, True))),
+        frozenset((Literal(Q.negative_infinite, True), Literal(Q.positive_infinite, True))),
         frozenset((Literal(Q.normal, False), Literal(Q.unitary, True))),
         frozenset((Literal(Q.normal, True), Literal(Q.square, False))),
-        frozenset((Literal(Q.orthogonal, False), Literal(Q.real, True), Literal(Q.unitary, True))),
+        frozenset((Literal(Q.odd, True), Literal(Q.rational, False))),
+        frozenset((Literal(Q.orthogonal, False), Literal(Q.real_elements, True), Literal(Q.unitary, True))),
         frozenset((Literal(Q.orthogonal, True), Literal(Q.positive_definite, False))),
         frozenset((Literal(Q.orthogonal, True), Literal(Q.unitary, False))),
         frozenset((Literal(Q.positive, False), Literal(Q.prime, True))),
-        frozenset((Literal(Q.positive, True), Literal(Q.real, False))),
         frozenset((Literal(Q.positive, True), Literal(Q.zero, True))),
-        frozenset((Literal(Q.rational, True), Literal(Q.real, False))),
-        frozenset((Literal(Q.real, False), Literal(Q.zero, True))),
         frozenset((Literal(Q.square, False), Literal(Q.symmetric, True))),
         frozenset((Literal(Q.triangular, False), Literal(Q.unit_triangular, True))),
         frozenset((Literal(Q.triangular, False), Literal(Q.upper_triangular, True)))
@@ -96,43 +89,29 @@ def get_known_facts_cnf():
         Q.invertible | Q.singular,
         Q.algebraic | ~Q.rational,
         Q.antihermitian | ~Q.imaginary,
+        Q.commutative | ~Q.finite,
+        Q.commutative | ~Q.infinite,
         Q.complex_elements | ~Q.real_elements,
-        Q.complex | ~Q.algebraic,
-        Q.complex | ~Q.imaginary,
-        Q.complex | ~Q.real,
-        Q.complex | ~Q.transcendental,
         Q.even | ~Q.zero,
-        Q.extended_real | ~Q.infinite,
-        Q.extended_real | ~Q.real,
         Q.finite | ~Q.algebraic,
-        Q.finite | ~Q.irrational,
-        Q.finite | ~Q.rational,
         Q.finite | ~Q.transcendental,
         Q.fullrank | ~Q.invertible,
-        Q.hermitian | ~Q.real,
-        Q.integer | ~Q.even,
-        Q.integer | ~Q.odd,
-        Q.integer | ~Q.prime,
+        Q.hermitian | ~Q.negative,
+        Q.hermitian | ~Q.positive,
+        Q.hermitian | ~Q.zero,
+        Q.infinite | ~Q.negative_infinite,
+        Q.infinite | ~Q.positive_infinite,
         Q.invertible | ~Q.positive_definite,
         Q.invertible | ~Q.unitary,
         Q.lower_triangular | ~Q.diagonal,
-        Q.nonnegative | ~Q.positive,
-        Q.nonnegative | ~Q.zero,
-        Q.nonpositive | ~Q.negative,
-        Q.nonpositive | ~Q.zero,
-        Q.nonzero | ~Q.negative,
-        Q.nonzero | ~Q.positive,
         Q.normal | ~Q.diagonal,
         Q.normal | ~Q.unitary,
         Q.positive_definite | ~Q.orthogonal,
+        Q.positive | ~Q.composite,
         Q.positive | ~Q.prime,
-        Q.rational | ~Q.integer,
+        Q.rational | ~Q.even,
+        Q.rational | ~Q.odd,
         Q.real_elements | ~Q.integer_elements,
-        Q.real | ~Q.irrational,
-        Q.real | ~Q.negative,
-        Q.real | ~Q.positive,
-        Q.real | ~Q.rational,
-        Q.real | ~Q.zero,
         Q.square | ~Q.invertible,
         Q.square | ~Q.normal,
         Q.square | ~Q.symmetric,
@@ -143,99 +122,98 @@ def get_known_facts_cnf():
         Q.unitary | ~Q.orthogonal,
         Q.upper_triangular | ~Q.diagonal,
         ~Q.algebraic | ~Q.transcendental,
-        ~Q.antihermitian | ~Q.hermitian,
         ~Q.composite | ~Q.prime,
         ~Q.even | ~Q.odd,
         ~Q.finite | ~Q.infinite,
-        ~Q.imaginary | ~Q.real,
+        ~Q.imaginary | ~Q.negative,
+        ~Q.imaginary | ~Q.positive,
+        ~Q.imaginary | ~Q.zero,
         ~Q.invertible | ~Q.singular,
         ~Q.irrational | ~Q.rational,
+        ~Q.negative_infinite | ~Q.positive_infinite,
         ~Q.negative | ~Q.positive,
         ~Q.negative | ~Q.zero,
         ~Q.positive | ~Q.zero,
-        Q.even | Q.odd | ~Q.integer,
-        Q.infinite | Q.real | ~Q.extended_real,
+        Q.algebraic | Q.transcendental | ~Q.imaginary,
+        Q.algebraic | Q.transcendental | ~Q.negative,
+        Q.algebraic | Q.transcendental | ~Q.positive,
+        Q.algebraic | Q.transcendental | ~Q.zero,
+        Q.antihermitian | Q.hermitian | ~Q.zero,
+        Q.even | Q.odd | ~Q.composite,
+        Q.even | Q.odd | ~Q.prime,
+        Q.irrational | Q.rational | ~Q.negative,
+        Q.irrational | Q.rational | ~Q.positive,
+        Q.irrational | Q.rational | ~Q.zero,
         Q.lower_triangular | Q.upper_triangular | ~Q.triangular,
-        Q.negative | Q.positive | ~Q.nonzero,
-        Q.negative | Q.zero | ~Q.nonpositive,
-        Q.positive | Q.zero | ~Q.nonnegative,
         Q.diagonal | ~Q.lower_triangular | ~Q.upper_triangular,
         Q.invertible | ~Q.fullrank | ~Q.square,
-        Q.orthogonal | ~Q.real | ~Q.unitary,
-        Q.negative | Q.positive | Q.zero | ~Q.real,
-        Q.algebraic | Q.transcendental | ~Q.complex | ~Q.finite,
-        Q.irrational | Q.rational | ~Q.finite | ~Q.real
+        Q.orthogonal | ~Q.real_elements | ~Q.unitary,
+        Q.negative | Q.positive | Q.zero | ~Q.irrational,
+        Q.negative | Q.positive | Q.zero | ~Q.rational,
+        Q.composite | Q.prime | ~Q.even | ~Q.positive
     )
 
 # -{ Known facts in compressed sets }-
+# This dictionary means that if a key is True, every item in its value is True.
 @cacheit
 def get_known_facts_dict():
     return {
-        Q.algebraic: set([Q.algebraic, Q.complex, Q.finite]),
+        Q.algebraic: set([Q.algebraic, Q.commutative, Q.finite]),
         Q.antihermitian: set([Q.antihermitian]),
         Q.commutative: set([Q.commutative]),
-        Q.complex: set([Q.complex]),
         Q.complex_elements: set([Q.complex_elements]),
-        Q.composite: set([Q.composite]),
+        Q.composite: set([Q.algebraic, Q.commutative, Q.composite, Q.finite,
+        Q.hermitian, Q.positive, Q.rational]),
         Q.diagonal: set([Q.diagonal, Q.lower_triangular, Q.normal, Q.square,
         Q.symmetric, Q.triangular, Q.upper_triangular]),
         Q.eq: set([Q.eq]),
-        Q.even: set([Q.algebraic, Q.complex, Q.even, Q.extended_real,
-        Q.finite, Q.hermitian, Q.integer, Q.rational, Q.real]),
-        Q.extended_real: set([Q.extended_real]),
-        Q.finite: set([Q.finite]),
+        Q.even: set([Q.algebraic, Q.commutative, Q.even, Q.finite,
+        Q.hermitian, Q.rational]),
+        Q.finite: set([Q.commutative, Q.finite]),
         Q.fullrank: set([Q.fullrank]),
         Q.ge: set([Q.ge]),
         Q.gt: set([Q.gt]),
         Q.hermitian: set([Q.hermitian]),
-        Q.imaginary: set([Q.antihermitian, Q.complex, Q.imaginary]),
-        Q.infinite: set([Q.extended_real, Q.infinite]),
-        Q.integer: set([Q.algebraic, Q.complex, Q.extended_real, Q.finite,
-        Q.hermitian, Q.integer, Q.rational, Q.real]),
+        Q.imaginary: set([Q.antihermitian, Q.commutative, Q.finite,
+        Q.imaginary]),
+        Q.infinite: set([Q.commutative, Q.infinite]),
         Q.integer_elements: set([Q.complex_elements, Q.integer_elements,
         Q.real_elements]),
         Q.invertible: set([Q.fullrank, Q.invertible, Q.square]),
-        Q.irrational: set([Q.complex, Q.extended_real, Q.finite, Q.hermitian,
-        Q.irrational, Q.nonzero, Q.real]),
+        Q.irrational: set([Q.commutative, Q.finite, Q.hermitian,
+        Q.irrational]),
         Q.is_true: set([Q.is_true]),
         Q.le: set([Q.le]),
         Q.lower_triangular: set([Q.lower_triangular, Q.triangular]),
         Q.lt: set([Q.lt]),
         Q.ne: set([Q.ne]),
-        Q.negative: set([Q.complex, Q.extended_real, Q.hermitian, Q.negative,
-        Q.nonpositive, Q.nonzero, Q.real]),
-        Q.nonnegative: set([Q.complex, Q.extended_real, Q.hermitian,
-        Q.nonnegative, Q.real]),
-        Q.nonpositive: set([Q.complex, Q.extended_real, Q.hermitian,
-        Q.nonpositive, Q.real]),
-        Q.nonzero: set([Q.complex, Q.extended_real, Q.hermitian, Q.nonzero,
-        Q.real]),
+        Q.negative: set([Q.commutative, Q.finite, Q.hermitian, Q.negative]),
+        Q.negative_infinite: set([Q.commutative, Q.infinite,
+        Q.negative_infinite]),
         Q.normal: set([Q.normal, Q.square]),
-        Q.odd: set([Q.algebraic, Q.complex, Q.extended_real, Q.finite,
-        Q.hermitian, Q.integer, Q.nonzero, Q.odd, Q.rational, Q.real]),
+        Q.odd: set([Q.algebraic, Q.commutative, Q.finite, Q.hermitian, Q.odd,
+        Q.rational]),
         Q.orthogonal: set([Q.fullrank, Q.invertible, Q.normal, Q.orthogonal,
         Q.positive_definite, Q.square, Q.unitary]),
-        Q.positive: set([Q.complex, Q.extended_real, Q.hermitian,
-        Q.nonnegative, Q.nonzero, Q.positive, Q.real]),
+        Q.positive: set([Q.commutative, Q.finite, Q.hermitian, Q.positive]),
         Q.positive_definite: set([Q.fullrank, Q.invertible,
         Q.positive_definite, Q.square]),
-        Q.prime: set([Q.algebraic, Q.complex, Q.extended_real, Q.finite,
-        Q.hermitian, Q.integer, Q.nonnegative, Q.nonzero, Q.positive,
-        Q.prime, Q.rational, Q.real]),
-        Q.rational: set([Q.algebraic, Q.complex, Q.extended_real, Q.finite,
-        Q.hermitian, Q.rational, Q.real]),
-        Q.real: set([Q.complex, Q.extended_real, Q.hermitian, Q.real]),
+        Q.positive_infinite: set([Q.commutative, Q.infinite,
+        Q.positive_infinite]),
+        Q.prime: set([Q.algebraic, Q.commutative, Q.finite, Q.hermitian,
+        Q.positive, Q.prime, Q.rational]),
+        Q.rational: set([Q.algebraic, Q.commutative, Q.finite, Q.hermitian,
+        Q.rational]),
         Q.real_elements: set([Q.complex_elements, Q.real_elements]),
         Q.singular: set([Q.singular]),
         Q.square: set([Q.square]),
         Q.symmetric: set([Q.square, Q.symmetric]),
-        Q.transcendental: set([Q.complex, Q.finite, Q.transcendental]),
+        Q.transcendental: set([Q.commutative, Q.finite, Q.transcendental]),
         Q.triangular: set([Q.triangular]),
         Q.unit_triangular: set([Q.triangular, Q.unit_triangular]),
         Q.unitary: set([Q.fullrank, Q.invertible, Q.normal, Q.square,
         Q.unitary]),
         Q.upper_triangular: set([Q.triangular, Q.upper_triangular]),
-        Q.zero: set([Q.algebraic, Q.complex, Q.even, Q.extended_real,
-        Q.finite, Q.hermitian, Q.integer, Q.nonnegative,
-        Q.nonpositive, Q.rational, Q.real, Q.zero]),
+        Q.zero: set([Q.algebraic, Q.commutative, Q.even, Q.finite,
+        Q.hermitian, Q.rational, Q.zero]),
     }
diff --git a/sympy/assumptions/cnf.py b/sympy/assumptions/cnf.py
index f5fb466d5768..f957f03fc52e 100644
--- a/sympy/assumptions/cnf.py
+++ b/sympy/assumptions/cnf.py
@@ -143,7 +143,27 @@ def to_NNF(expr):
     """
     Generates the Negation Normal Form of any boolean expression in terms
     of AND, OR, and Literal objects.
+
+    Examples
+    ========
+
+    >>> from sympy import Q
+    >>> from sympy.assumptions.cnf import to_NNF
+    >>> from sympy.abc import x
+    >>> expr = Q.even(x) & ~Q.positive(x)
+    >>> to_NNF(expr)
+    (Literal(Q.even(x), False) & Literal(Q.positive(x), True))
+
+    ``to_NNF`` decomposes the predicate into a combination of primitive
+    predicates if possible.
+
+    >>> to_NNF(Q.nonpositive)
+    (Literal(Q.negative, False) | Literal(Q.zero, False))
+    >>> to_NNF(Q.nonpositive(x))
+    (Literal(Q.negative(x), False) | Literal(Q.zero(x), False))
     """
+    from sympy.assumptions.assume import AppliedPredicate, Predicate
+    from sympy.assumptions.facts import get_composite_predicates
 
     if isinstance(expr, Not):
         arg = expr.args[0]
@@ -200,8 +220,20 @@ def to_NNF(expr):
         R = to_NNF(expr.args[2])
         return AND(OR(~L, M), OR(L, R))
 
-    else:
-        return Literal(expr)
+    if isinstance(expr, AppliedPredicate):
+        comp_dct = get_composite_predicates()
+        pred, args = expr.function, expr.arguments
+        newpred = comp_dct.get(pred, None)
+        if newpred is not None:
+            return to_NNF(newpred.rcall(*args))
+
+    if isinstance(expr, Predicate):
+        comp_dct = get_composite_predicates()
+        newpred = comp_dct.get(expr, None)
+        if newpred is not None:
+            return to_NNF(newpred)
+
+    return Literal(expr)
 
 
 def distribute_AND_over_OR(expr):
@@ -238,7 +270,9 @@ class CNF:
     >>> from sympy.abc import x
     >>> cnf = CNF.from_prop(Q.real(x) & ~Q.zero(x))
     >>> cnf.clauses
-    {frozenset({Literal(Q.real(x), False)}), frozenset({Literal(Q.zero(x), True)})}
+    {frozenset({Literal(Q.zero(x), True)}),
+    frozenset({Literal(Q.negative(x), False),
+    Literal(Q.positive(x), False), Literal(Q.zero(x), False)})}
     """
     def __init__(self, clauses=None):
         if not clauses:
@@ -318,8 +352,6 @@ def rcall(self, expr):
         expr = AND(*clause_list)
         return distribute_AND_over_OR(expr)
 
-
-
     @classmethod
     def all_or(cls, *cnfs):
         b = cnfs[0].copy()
diff --git a/sympy/assumptions/facts.py b/sympy/assumptions/facts.py
new file mode 100644
index 000000000000..3fd3d7ed247d
--- /dev/null
+++ b/sympy/assumptions/facts.py
@@ -0,0 +1,208 @@
+"""
+Known facts in assumptions module.
+
+This module defines the facts in ``get_known_facts()``, and supports functions
+to generate the contents in ``sympy.assumptions.ask_generated`` file.
+"""
+
+from sympy.core.cache import cacheit
+from sympy.assumptions import Q
+from sympy.assumptions.cnf import CNF
+from sympy.logic.boolalg import (to_cnf, And, Not, Implies, Equivalent)
+from sympy.logic.inference import satisfiable
+
+
+@cacheit
+def get_composite_predicates():
+    # To reduce the complexity of sat solver, these predicates never goes into facts
+    # but are transformed into the combination of primitive predicates.
+    return {
+        Q.real : Q.negative | Q.zero | Q.positive,
+        Q.integer : Q.even | Q.odd,
+        Q.nonpositive : Q.negative | Q.zero,
+        Q.nonzero : Q.negative | Q.positive,
+        Q.nonnegative : Q.zero | Q.positive,
+        Q.extended_real : Q.negative_infinite | Q.negative | Q.zero | Q.positive | Q.positive_infinite,
+        Q.extended_positive: Q.positive | Q.positive_infinite,
+        Q.extended_negative: Q.negative | Q.negative_infinite,
+        Q.extended_nonzero: Q.negative_infinite | Q.negative | Q.positive | Q.positive_infinite,
+        Q.extended_nonpositive: Q.negative_infinite | Q.negative | Q.zero,
+        Q.extended_nonnegative: Q.zero | Q.positive | Q.positive_infinite,
+        Q.complex : Q.algebraic | Q.transcendental
+    }
+
+
+@cacheit
+def get_known_facts():
+    # We build the facts starting with primitive predicates.
+    # DO NOT include the predicates in get_composite_predicates()'s keys here!
+    return And(
+
+        # primitive predicates exclude each other
+        Implies(Q.negative_infinite, ~Q.positive_infinite),
+        Implies(Q.negative, ~Q.zero & ~Q.positive),
+        Implies(Q.positive, ~Q.zero),
+
+        # build real line and complex plane
+        Implies(Q.negative | Q.zero | Q.positive, ~Q.imaginary),
+        Implies(Q.negative | Q.zero | Q.positive | Q.imaginary, Q.algebraic | Q.transcendental),
+
+        # other subsets of complex
+        Implies(Q.transcendental, ~Q.algebraic),
+        Implies(Q.irrational, ~Q.rational),
+        Equivalent(Q.rational | Q.irrational, Q.negative | Q.zero | Q.positive),
+        Implies(Q.rational, Q.algebraic),
+
+        # integers
+        Implies(Q.even, ~Q.odd),
+        Implies(Q.even | Q.odd, Q.rational),
+        Implies(Q.zero, Q.even),
+        Implies(Q.composite, ~Q.prime),
+        Implies(Q.composite | Q.prime, (Q.even | Q.odd) & Q.positive),
+        Implies(Q.even & Q.positive & ~Q.prime, Q.composite),
+
+        # hermitian and antihermitian
+        Implies(Q.negative | Q.zero | Q.positive, Q.hermitian),
+        Implies(Q.imaginary, Q.antihermitian),
+        Implies(Q.zero, Q.hermitian | Q.antihermitian),
+
+        # define finity and infinity, and build extended real line
+        Implies(Q.infinite, ~Q.finite),
+        Implies(Q.algebraic | Q.transcendental, Q.finite),
+        Implies(Q.negative_infinite | Q.positive_infinite, Q.infinite),
+
+        # commutativity
+        Implies(Q.finite | Q.infinite, Q.commutative),
+
+        # matrices
+        Implies(Q.orthogonal, Q.positive_definite),
+        Implies(Q.orthogonal, Q.unitary),
+        Implies(Q.unitary & Q.real_elements, Q.orthogonal),
+        Implies(Q.unitary, Q.normal),
+        Implies(Q.unitary, Q.invertible),
+        Implies(Q.normal, Q.square),
+        Implies(Q.diagonal, Q.normal),
+        Implies(Q.positive_definite, Q.invertible),
+        Implies(Q.diagonal, Q.upper_triangular),
+        Implies(Q.diagonal, Q.lower_triangular),
+        Implies(Q.lower_triangular, Q.triangular),
+        Implies(Q.upper_triangular, Q.triangular),
+        Implies(Q.triangular, Q.upper_triangular | Q.lower_triangular),
+        Implies(Q.upper_triangular & Q.lower_triangular, Q.diagonal),
+        Implies(Q.diagonal, Q.symmetric),
+        Implies(Q.unit_triangular, Q.triangular),
+        Implies(Q.invertible, Q.fullrank),
+        Implies(Q.invertible, Q.square),
+        Implies(Q.symmetric, Q.square),
+        Implies(Q.fullrank & Q.square, Q.invertible),
+        Equivalent(Q.invertible, ~Q.singular),
+        Implies(Q.integer_elements, Q.real_elements),
+        Implies(Q.real_elements, Q.complex_elements),
+    )
+
+
+@cacheit
+def get_known_facts_keys():
+    result = []
+    exclude = get_composite_predicates()
+    for attr in Q.__class__.__dict__:
+        if attr.startswith('__'):
+            continue
+        pred = getattr(Q, attr)
+        if pred in exclude:
+            continue
+        result.append(pred)
+    return result
+
+
+def compute_known_facts(known_facts, known_facts_keys):
+    """Compute the various forms of knowledge compilation used by the
+    assumptions system.
+
+    Explanation
+    ===========
+
+    This function is typically applied to the results of the ``get_known_facts``
+    and ``get_known_facts_keys`` functions defined at the bottom of
+    this file.
+    """
+    from textwrap import dedent, wrap
+
+    fact_string = dedent('''\
+    """
+    The contents of this file are the return value of
+    ``sympy.assumptions.ask.compute_known_facts``.
+
+    Do NOT manually edit this file.
+    Instead, run ./bin/ask_update.py.
+    """
+
+    from sympy.core.cache import cacheit
+    from sympy.logic.boolalg import And
+    from sympy.assumptions.cnf import Literal
+    from sympy.assumptions.ask import Q
+
+    # -{ Known facts as a set }-
+    @cacheit
+    def get_all_known_facts():
+        return {
+            %s
+        }
+
+    # -{ Known facts in Conjunctive Normal Form }-
+    @cacheit
+    def get_known_facts_cnf():
+        return And(
+            %s
+        )
+
+    # -{ Known facts in compressed sets }-
+    # This dictionary means that if a key is True, every item in its value is True.
+    @cacheit
+    def get_known_facts_dict():
+        return {
+            %s
+        }
+    ''')
+    # Compute the known facts in CNF form for logical inference
+    LINE = ",\n        "
+    HANG = ' '*8
+    cnf = to_cnf(known_facts)
+    cnf_ = CNF.to_CNF(known_facts)
+    c = LINE.join([str(a) for a in cnf.args])
+
+    p = LINE.join(sorted(['frozenset((' + ', '.join(str(lit) for lit in sorted(clause, key=str)) +'))' for clause in cnf_.clauses]))
+    mapping = single_fact_lookup(known_facts_keys, cnf)
+    items = sorted(mapping.items(), key=str)
+    keys = [str(i[0]) for i in items]
+    values = ['set(%s)' % sorted(i[1], key=str) for i in items]
+    m = LINE.join(['\n'.join(
+        wrap("{}: {}".format(k, v),
+            subsequent_indent=HANG,
+            break_long_words=False))
+        for k, v in zip(keys, values)]) + ','
+    return fact_string % (p, c, m)
+
+
+def single_fact_lookup(known_facts_keys, known_facts_cnf):
+    # Compute the quick lookup for single facts
+    mapping = {}
+    for key in known_facts_keys:
+        mapping[key] = {key}
+        for other_key in known_facts_keys:
+            if other_key != key:
+                if ask_full_inference(other_key, key, known_facts_cnf):
+                    mapping[key].add(other_key)
+    return mapping
+
+
+def ask_full_inference(proposition, assumptions, known_facts_cnf):
+    """
+    Method for inferring properties about objects.
+
+    """
+    if not satisfiable(And(known_facts_cnf, assumptions, proposition)):
+        return False
+    if not satisfiable(And(known_facts_cnf, assumptions, Not(proposition))):
+        return True
+    return None
diff --git a/sympy/assumptions/handlers/calculus.py b/sympy/assumptions/handlers/calculus.py
index 4ae13d71a80d..71293b58afe5 100644
--- a/sympy/assumptions/handlers/calculus.py
+++ b/sympy/assumptions/handlers/calculus.py
@@ -10,7 +10,8 @@
 from sympy.functions import cos, exp, log, sign, sin
 from sympy.logic.boolalg import conjuncts
 
-from ..predicates.calculus import FinitePredicate, InfinitePredicate
+from ..predicates.calculus import (FinitePredicate, InfinitePredicate,
+    PositiveInfinitePredicate, NegativeInfinitePredicate)
 
 
 # FinitePredicate
@@ -95,7 +96,7 @@ def _(expr, assumptions):
         _bounded = ask(Q.finite(arg), assumptions)
         if _bounded:
             continue
-        s = ask(Q.positive(arg), assumptions)
+        s = ask(Q.extended_positive(arg), assumptions)
         # if there has been more than one sign or if the sign of this arg
         # is None and Bounded is None or there was already
         # an unknown sign, return None
@@ -228,3 +229,29 @@ def _(expr, assumptions):
 @InfinitePredicate.register_many(ComplexInfinity, Infinity, NegativeInfinity)
 def _(expr, assumptions):
     return True
+
+
+# PositiveInfinitePredicate
+
+
+@PositiveInfinitePredicate.register(Infinity)
+def _(expr, assumptions):
+    return True
+
+
+@PositiveInfinitePredicate.register_many(NegativeInfinity, ComplexInfinity)
+def _(expr, assumptions):
+    return False
+
+
+# NegativeInfinitePredicate
+
+
+@NegativeInfinitePredicate.register(NegativeInfinity)
+def _(expr, assumptions):
+    return True
+
+
+@NegativeInfinitePredicate.register_many(Infinity, ComplexInfinity)
+def _(expr, assumptions):
+    return False
diff --git a/sympy/assumptions/handlers/order.py b/sympy/assumptions/handlers/order.py
index 7b3bc758974c..6f2581e606a3 100644
--- a/sympy/assumptions/handlers/order.py
+++ b/sympy/assumptions/handlers/order.py
@@ -13,7 +13,10 @@
 from sympy.multipledispatch import MDNotImplementedError
 
 from ..predicates.order import (NegativePredicate, NonNegativePredicate,
-    NonZeroPredicate, ZeroPredicate, NonPositivePredicate, PositivePredicate)
+    NonZeroPredicate, ZeroPredicate, NonPositivePredicate, PositivePredicate,
+    ExtendedNegativePredicate, ExtendedNonNegativePredicate,
+    ExtendedNonPositivePredicate, ExtendedNonZeroPredicate,
+    ExtendedPositivePredicate,)
 
 
 # NegativePredicate
@@ -392,3 +395,44 @@ def _(expr, assumptions):
 @PositivePredicate.register(NaN)
 def _(expr, assumptions):
     return None
+
+
+# ExtendedNegativePredicate
+
+@ExtendedNegativePredicate.register(object)
+def _(expr, assumptions):
+    return ask(Q.negative(expr) | Q.negative_infinite(expr), assumptions)
+
+
+# ExtendedPositivePredicate
+
+@ExtendedPositivePredicate.register(object)
+def _(expr, assumptions):
+    return ask(Q.positive(expr) | Q.positive_infinite(expr), assumptions)
+
+
+# ExtendedNonZeroPredicate
+
+@ExtendedNonZeroPredicate.register(object)
+def _(expr, assumptions):
+    return ask(
+        Q.negative_infinite(expr) | Q.negative(expr) | Q.positive(expr) | Q.positive_infinite(expr),
+        assumptions)
+
+
+# ExtendedNonPositivePredicate
+
+@ExtendedNonPositivePredicate.register(object)
+def _(expr, assumptions):
+    return ask(
+        Q.negative_infinite(expr) | Q.negative(expr) | Q.zero(expr),
+        assumptions)
+
+
+# ExtendedNonNegativePredicate
+
+@ExtendedNonNegativePredicate.register(object)
+def _(expr, assumptions):
+    return ask(
+        Q.zero(expr) | Q.positive(expr) | Q.positive_infinite(expr),
+        assumptions)
diff --git a/sympy/assumptions/handlers/sets.py b/sympy/assumptions/handlers/sets.py
index bc1487960cf6..8911bc0f1d95 100644
--- a/sympy/assumptions/handlers/sets.py
+++ b/sympy/assumptions/handlers/sets.py
@@ -638,6 +638,8 @@ def _(expr, assumptions):
 def _(expr, assumptions):
     if isinstance(expr, MatrixBase):
         return None
+    if ask(Q.zero(expr), assumptions):
+        return True
     return ask(Q.imaginary(expr), assumptions)
 
 @AntihermitianPredicate.register(Add)
diff --git a/sympy/assumptions/predicates/calculus.py b/sympy/assumptions/predicates/calculus.py
index d0ad129bef48..f30070378868 100644
--- a/sympy/assumptions/predicates/calculus.py
+++ b/sympy/assumptions/predicates/calculus.py
@@ -27,8 +27,8 @@ class FinitePredicate(Predicate):
     True
     >>> ask(Q.finite(2 + 3*I))
     True
-    >>> print(ask(Q.finite(x), Q.positive(x)))
-    None
+    >>> ask(Q.finite(x), Q.positive(x))
+    True
     >>> print(ask(Q.finite(S.NaN)))
     None
 
@@ -60,3 +60,23 @@ class InfinitePredicate(Predicate):
         "InfiniteHandler",
         doc="""Handler for Q.infinite key."""
     )
+
+
+class PositiveInfinitePredicate(Predicate):
+    """
+    Positive infinity predicate.
+
+    ``Q.positive_infinite(x)`` is true iff ``x`` is positive infinity ``oo``.
+    """
+    name = 'positive_infinite'
+    handler = Dispatcher("PositiveInfiniteHandler")
+
+
+class NegativeInfinitePredicate(Predicate):
+    """
+    Negative infinity predicate.
+
+    ``Q.negative_infinite(x)`` is true iff ``x`` is negative infinity ``-oo``.
+    """
+    name = 'negative_infinite'
+    handler = Dispatcher("NegativeInfiniteHandler")
diff --git a/sympy/assumptions/predicates/order.py b/sympy/assumptions/predicates/order.py
index e183ecc8d57d..372eda329325 100644
--- a/sympy/assumptions/predicates/order.py
+++ b/sympy/assumptions/predicates/order.py
@@ -254,3 +254,137 @@ class PositivePredicate(Predicate):
         doc=("Handler for key 'positive'. Test that an expression is strictly"
         " greater than zero.")
     )
+
+
+class ExtendedPositivePredicate(Predicate):
+    r"""
+    Positive extended real number predicate.
+
+    Explanation
+    ===========
+
+    ``Q.extended_positive(x)`` is true iff ``x`` is extended real and
+    `x > 0`, that is if ``x`` is in the interval `(0, \infty]`.
+
+    Examples
+    ========
+
+    >>> from sympy import ask, I, oo, Q
+    >>> ask(Q.extended_positive(1))
+    True
+    >>> ask(Q.extended_positive(oo))
+    True
+    >>> ask(Q.extended_positive(I))
+    False
+
+    """
+    name = 'extended_positive'
+    handler = Dispatcher("ExtendedPositiveHandler")
+
+
+class ExtendedNegativePredicate(Predicate):
+    r"""
+    Negative extended real number predicate.
+
+    Explanation
+    ===========
+
+    ``Q.extended_negative(x)`` is true iff ``x`` is extended real and
+    `x < 0`, that is if ``x`` is in the interval `[-\infty, 0)`.
+
+    Examples
+    ========
+
+    >>> from sympy import ask, I, oo, Q
+    >>> ask(Q.extended_negative(-1))
+    True
+    >>> ask(Q.extended_negative(-oo))
+    True
+    >>> ask(Q.extended_negative(-I))
+    False
+
+    """
+    name = 'extended_negative'
+    handler = Dispatcher("ExtendedNegativeHandler")
+
+
+class ExtendedNonZeroPredicate(Predicate):
+    """
+    Nonzero extended real number predicate.
+
+    Explanation
+    ===========
+
+    ``ask(Q.extended_nonzero(x))`` is true iff ``x`` is extended real and
+    ``x`` is not zero.
+
+    Examples
+    ========
+
+    >>> from sympy import ask, I, oo, Q
+    >>> ask(Q.extended_nonzero(-1))
+    True
+    >>> ask(Q.extended_nonzero(oo))
+    True
+    >>> ask(Q.extended_nonzero(I))
+    False
+
+    """
+    name = 'extended_nonzero'
+    handler = Dispatcher("ExtendedNonZeroHandler")
+
+
+class ExtendedNonPositivePredicate(Predicate):
+    """
+    Nonpositive extended real number predicate.
+
+    Explanation
+    ===========
+
+    ``ask(Q.extended_nonpositive(x))`` is true iff ``x`` is extended real and
+    ``x`` is not positive.
+
+    Examples
+    ========
+
+    >>> from sympy import ask, I, oo, Q
+    >>> ask(Q.extended_nonpositive(-1))
+    True
+    >>> ask(Q.extended_nonpositive(oo))
+    False
+    >>> ask(Q.extended_nonpositive(0))
+    True
+    >>> ask(Q.extended_nonpositive(I))
+    False
+
+    """
+    name = 'extended_nonpositive'
+    handler = Dispatcher("ExtendedNonPositiveHandler")
+
+
+class ExtendedNonNegativePredicate(Predicate):
+    """
+    Nonnegative extended real number predicate.
+
+    Explanation
+    ===========
+
+    ``ask(Q.extended_nonnegative(x))`` is true iff ``x`` is extended real and
+    ``x`` is not negative.
+
+    Examples
+    ========
+
+    >>> from sympy import ask, I, oo, Q
+    >>> ask(Q.extended_nonnegative(-1))
+    False
+    >>> ask(Q.extended_nonnegative(oo))
+    True
+    >>> ask(Q.extended_nonnegative(0))
+    True
+    >>> ask(Q.extended_nonnegative(I))
+    False
+
+    """
+    name = 'extended_nonnegative'
+    handler = Dispatcher("ExtendedNonNegativeHandler")
diff --git a/sympy/assumptions/tests/test_query.py b/sympy/assumptions/tests/test_query.py
index 4e010cca0b20..2189ef93c557 100644
--- a/sympy/assumptions/tests/test_query.py
+++ b/sympy/assumptions/tests/test_query.py
@@ -2,7 +2,7 @@
 from sympy.assumptions import (ask, AssumptionsContext, Q, register_handler,
         remove_handler)
 from sympy.assumptions.assume import assuming, global_assumptions, Predicate
-from sympy.assumptions.ask import compute_known_facts, single_fact_lookup
+from sympy.assumptions.facts import compute_known_facts, single_fact_lookup
 from sympy.assumptions.handlers import AskHandler
 from sympy.core.add import Add
 from sympy.core.numbers import (I, Integer, Rational, oo, zoo, pi)
@@ -140,7 +140,7 @@ def test_zero_0():
     assert ask(Q.prime(z)) is False
     assert ask(Q.composite(z)) is False
     assert ask(Q.hermitian(z)) is True
-    assert ask(Q.antihermitian(z)) is False
+    assert ask(Q.antihermitian(z)) is True
 
 
 def test_negativeone():
@@ -176,7 +176,7 @@ def test_infinity():
     assert ask(Q.irrational(oo)) is False
     assert ask(Q.imaginary(oo)) is False
     assert ask(Q.positive(oo)) is False
-    #assert ask(Q.extended_positive(oo)) is True
+    assert ask(Q.extended_positive(oo)) is True
     assert ask(Q.negative(oo)) is False
     assert ask(Q.even(oo)) is False
     assert ask(Q.odd(oo)) is False
@@ -186,6 +186,8 @@ def test_infinity():
     assert ask(Q.composite(oo)) is False
     assert ask(Q.hermitian(oo)) is False
     assert ask(Q.antihermitian(oo)) is False
+    assert ask(Q.positive_infinite(oo)) is True
+    assert ask(Q.negative_infinite(oo)) is False
 
 
 def test_neg_infinity():
@@ -201,7 +203,7 @@ def test_neg_infinity():
     assert ask(Q.imaginary(mm)) is False
     assert ask(Q.positive(mm)) is False
     assert ask(Q.negative(mm)) is False
-    #assert ask(Q.extended_negative(mm)) is True
+    assert ask(Q.extended_negative(mm)) is True
     assert ask(Q.even(mm)) is False
     assert ask(Q.odd(mm)) is False
     assert ask(Q.finite(mm)) is False
@@ -210,6 +212,8 @@ def test_neg_infinity():
     assert ask(Q.composite(mm)) is False
     assert ask(Q.hermitian(mm)) is False
     assert ask(Q.antihermitian(mm)) is False
+    assert ask(Q.positive_infinite(-oo)) is False
+    assert ask(Q.negative_infinite(-oo)) is True
 
 
 def test_complex_infinity():
@@ -234,6 +238,8 @@ def test_complex_infinity():
     assert ask(Q.composite(zoo)) is False
     assert ask(Q.hermitian(zoo)) is False
     assert ask(Q.antihermitian(zoo)) is False
+    assert ask(Q.positive_infinite(zoo)) is False
+    assert ask(Q.negative_infinite(zoo)) is False
 
 
 def test_nan():
@@ -595,13 +601,13 @@ def test_I():
     assert ask(Q.real(z)) is True
 
 
-
+@XFAIL  # definition for boundedness fixed! will be changed in next commit
 def test_bounded():
     x, y, z = symbols('x,y,z')
     assert ask(Q.finite(x)) is None
     assert ask(Q.finite(x), Q.finite(x)) is True
     assert ask(Q.finite(x), Q.finite(y)) is None
-    assert ask(Q.finite(x), Q.complex(x)) is None
+    assert ask(Q.finite(x), Q.complex(x)) is True
 
     assert ask(Q.finite(x + 1)) is None
     assert ask(Q.finite(x + 1), Q.finite(x)) is True
@@ -610,7 +616,7 @@ def test_bounded():
     # B + B
     assert ask(Q.finite(a), Q.finite(x) & Q.finite(y)) is True
     assert ask(
-        Q.finite(a), Q.finite(x) & Q.finite(y) & Q.positive(x)) is True
+        Q.finite(a), Q.positive(x) & Q.finite(y)) is True
     assert ask(
         Q.finite(a), Q.finite(x) & Q.finite(y) & Q.positive(y)) is True
     assert ask(Q.finite(a),
@@ -1354,12 +1360,13 @@ def test_rational():
 
 def test_hermitian():
     assert ask(Q.hermitian(x)) is None
-    assert ask(Q.hermitian(x), Q.antihermitian(x)) is False
+    assert ask(Q.hermitian(x), Q.antihermitian(x)) is None
     assert ask(Q.hermitian(x), Q.imaginary(x)) is False
     assert ask(Q.hermitian(x), Q.prime(x)) is True
     assert ask(Q.hermitian(x), Q.real(x)) is True
+    assert ask(Q.hermitian(x), Q.zero(x)) is True
 
-    assert ask(Q.hermitian(x + 1), Q.antihermitian(x)) is False
+    assert ask(Q.hermitian(x + 1), Q.antihermitian(x)) is None
     assert ask(Q.hermitian(x + 1), Q.complex(x)) is None
     assert ask(Q.hermitian(x + 1), Q.hermitian(x)) is True
     assert ask(Q.hermitian(x + 1), Q.imaginary(x)) is False
@@ -1373,9 +1380,9 @@ def test_hermitian():
         Q.hermitian(x + y), Q.antihermitian(x) & Q.antihermitian(y)) is None
     assert ask(Q.hermitian(x + y), Q.antihermitian(x) & Q.complex(y)) is None
     assert ask(
-        Q.hermitian(x + y), Q.antihermitian(x) & Q.hermitian(y)) is False
+        Q.hermitian(x + y), Q.antihermitian(x) & Q.hermitian(y)) is None
     assert ask(Q.hermitian(x + y), Q.antihermitian(x) & Q.imaginary(y)) is None
-    assert ask(Q.hermitian(x + y), Q.antihermitian(x) & Q.real(y)) is False
+    assert ask(Q.hermitian(x + y), Q.antihermitian(x) & Q.real(y)) is None
     assert ask(Q.hermitian(x + y), Q.hermitian(x) & Q.complex(y)) is None
     assert ask(Q.hermitian(x + y), Q.hermitian(x) & Q.hermitian(y)) is True
     assert ask(Q.hermitian(x + y), Q.hermitian(x) & Q.imaginary(y)) is False
@@ -1410,12 +1417,13 @@ def test_hermitian():
     assert ask(Q.antihermitian(x + 1), Q.complex(x)) is None
     assert ask(Q.antihermitian(x + 1), Q.hermitian(x)) is None
     assert ask(Q.antihermitian(x + 1), Q.imaginary(x)) is False
-    assert ask(Q.antihermitian(x + 1), Q.real(x)) is False
+    assert ask(Q.antihermitian(x + 1), Q.real(x)) is None
     assert ask(Q.antihermitian(x + I), Q.antihermitian(x)) is True
     assert ask(Q.antihermitian(x + I), Q.complex(x)) is None
-    assert ask(Q.antihermitian(x + I), Q.hermitian(x)) is False
+    assert ask(Q.antihermitian(x + I), Q.hermitian(x)) is None
     assert ask(Q.antihermitian(x + I), Q.imaginary(x)) is True
     assert ask(Q.antihermitian(x + I), Q.real(x)) is False
+    assert ask(Q.antihermitian(x), Q.zero(x)) is True
 
     assert ask(
         Q.antihermitian(x + y), Q.antihermitian(x) & Q.antihermitian(y)
@@ -1423,7 +1431,7 @@ def test_hermitian():
     assert ask(
         Q.antihermitian(x + y), Q.antihermitian(x) & Q.complex(y)) is None
     assert ask(
-        Q.antihermitian(x + y), Q.antihermitian(x) & Q.hermitian(y)) is False
+        Q.antihermitian(x + y), Q.antihermitian(x) & Q.hermitian(y)) is None
     assert ask(
         Q.antihermitian(x + y), Q.antihermitian(x) & Q.imaginary(y)) is True
     assert ask(Q.antihermitian(x + y), Q.antihermitian(x) & Q.real(y)
@@ -1432,13 +1440,13 @@ def test_hermitian():
     assert ask(Q.antihermitian(x + y), Q.hermitian(x) & Q.hermitian(y)
         ) is None
     assert ask(
-        Q.antihermitian(x + y), Q.hermitian(x) & Q.imaginary(y)) is False
+        Q.antihermitian(x + y), Q.hermitian(x) & Q.imaginary(y)) is None
     assert ask(Q.antihermitian(x + y), Q.hermitian(x) & Q.real(y)) is None
     assert ask(Q.antihermitian(x + y), Q.imaginary(x) & Q.complex(y)) is None
     assert ask(Q.antihermitian(x + y), Q.imaginary(x) & Q.imaginary(y)) is True
     assert ask(Q.antihermitian(x + y), Q.imaginary(x) & Q.real(y)) is False
     assert ask(Q.antihermitian(x + y), Q.real(x) & Q.complex(y)) is None
-    assert ask(Q.antihermitian(x + y), Q.real(x) & Q.real(y)) is False
+    assert ask(Q.antihermitian(x + y), Q.real(x) & Q.real(y)) is None
 
     assert ask(Q.antihermitian(I*x), Q.real(x)) is True
     assert ask(Q.antihermitian(I*x), Q.antihermitian(x)) is False
@@ -1446,7 +1454,7 @@ def test_hermitian():
     assert ask(Q.antihermitian(x*y), Q.antihermitian(x) & Q.real(y)) is True
 
     assert ask(Q.antihermitian(x + y + z),
-        Q.real(x) & Q.real(y) & Q.real(z)) is False
+        Q.real(x) & Q.real(y) & Q.real(z)) is None
     assert ask(Q.antihermitian(x + y + z),
         Q.real(x) & Q.real(y) & Q.imaginary(z)) is None
     assert ask(Q.antihermitian(x + y + z),
@@ -2130,7 +2138,7 @@ def test_compute_known_facts():
 @slow
 def test_known_facts_consistent():
     """"Test that ask_generated.py is up-to-date"""
-    from sympy.assumptions.ask import get_known_facts, get_known_facts_keys
+    from sympy.assumptions.facts import get_known_facts, get_known_facts_keys
     from os.path import abspath, dirname, join
     filename = join(dirname(dirname(abspath(__file__))), 'ask_generated.py')
     with open(filename) as f:
diff --git a/sympy/core/tests/test_args.py b/sympy/core/tests/test_args.py
index 6ce543c84f1d..8066fd527e3e 100644
--- a/sympy/core/tests/test_args.py
+++ b/sympy/core/tests/test_args.py
@@ -96,7 +96,6 @@ def _test_args(obj):
 
 def test_sympy__assumptions__assume__AppliedPredicate():
     from sympy.assumptions.assume import AppliedPredicate, Predicate
-    from sympy import Q
     assert _test_args(AppliedPredicate(Predicate("test"), 2))
     assert _test_args(Q.is_true(True))
 
@@ -105,8 +104,10 @@ def test_sympy__assumptions__assume__Predicate():
     pass
 
 def test_predicates():
-    from sympy.assumptions.ask import get_known_facts_keys
-    predicates = get_known_facts_keys()
+    predicates = [
+        getattr(Q, attr)
+        for attr in Q.__class__.__dict__
+        if not attr.startswith('__')]
     for p in predicates:
         assert _test_args(p)
 
@@ -123,38 +124,31 @@ def test_sympy__assumptions__relation__binrel__AppliedBinaryRelation():
 
 def test_sympy__assumptions__sathandlers__UnevaluatedOnFree():
     from sympy.assumptions.sathandlers import UnevaluatedOnFree
-    from sympy import Q
     assert _test_args(UnevaluatedOnFree(Q.positive))
 
 def test_sympy__assumptions__sathandlers__AllArgs():
     from sympy.assumptions.sathandlers import AllArgs
-    from sympy import Q
     assert _test_args(AllArgs(Q.positive))
 
 def test_sympy__assumptions__sathandlers__AnyArgs():
     from sympy.assumptions.sathandlers import AnyArgs
-    from sympy import Q
     assert _test_args(AnyArgs(Q.positive))
 
 def test_sympy__assumptions__sathandlers__ExactlyOneArg():
     from sympy.assumptions.sathandlers import ExactlyOneArg
-    from sympy import Q
     assert _test_args(ExactlyOneArg(Q.positive))
 
 def test_sympy__assumptions__sathandlers__CheckOldAssump():
     from sympy.assumptions.sathandlers import CheckOldAssump
-    from sympy import Q
     assert _test_args(CheckOldAssump(Q.positive))
 
 def test_sympy__assumptions__sathandlers__CheckIsPrime():
     from sympy.assumptions.sathandlers import CheckIsPrime
-    from sympy import Q
     # Input must be a number
     assert _test_args(CheckIsPrime(Q.positive))
 
 def test_sympy__assumptions__wrapper__AssumptionsWrapper():
     from sympy.assumptions.wrapper import AssumptionsWrapper
-    from sympy import Q
     assert _test_args(AssumptionsWrapper(x, Q.positive(x)))
 
 


Code review comments:
diff_hunk: @@ -143,7 +143,27 @@ def to_NNF(expr):
     """
     Generates the Negation Normal Form of any boolean expression in terms
     of AND, OR, and Literal objects.
+
+    Examples
+    ========
+
+    >>> from sympy import Q
+    >>> from sympy.assumptions.cnf import to_NNF
+    >>> from sympy.abc import x
+    >>> expr = Q.even(x) & ~Q.positive(x)
+    >>> to_NNF(expr)
+    (Literal(Q.even(x), False) & Literal(Q.positive(x), True))
+
+    ``to_NNF`` decomposes the predicate into a combination of primitive
+    predicates if possible.
path: sympy/assumptions/cnf.py
text: @user1:
It doesn't seem like this belongs as part of the `to_NNF` function.

@author:
Do you mean that predicate decomposition should be done by some other function?

@user1:
It just seems messy to me to do it as part of this function which has a clearly defined purpose: take a logical expression and convert it to NNF (without applying any interpretation to the meaning of the literals).

@author:
What about giving keyword argument `decompose=True/False` to this function?

@user1:
Perhaps it could take a `composite_map` argument or something like that.

@author:
Done.