Complex

Simplification#

Simplification for complex formulas.

Note

The function simplify() implements simplification for the theory of complex numbers. It takes a formula as input and returns an equivalent simplified formula modulo optional assumptions.

>>> from logic1.firstorder import *
>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> simplify(And(z**2 == 1, Re(z) > 0))
z - 1 == 0
>>> simplify(Re(z) == 0, assume=[Im(z) == 1])
z - I == 0

The function is_valid() heuristically checks whether a formula is valid, i.e. the formula holds for all possible values of its free variables. In case the validity of the formula cannot be determined, the function returns None.

>>> from logic1.firstorder import *
>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> is_valid(z * ~z >= 0)
True
>>> is_valid(Re(z) > 0, assume=[z == 0])
False
>>> print(is_valid(z == 0))
None

User Interface#

Return a simplified formula that is equivalent to the given formula using the given assumptions and options. The options are directly passed to RCF.simplify.simplify(), which is used internally.

>>> from logic1.firstorder import *
>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> simplify(And(z**2 == 1, Re(z) > 0))
z - 1 == 0
>>> simplify(Re(z) == 0, assume=[Im(z) == 1])
z - I == 0

Return True if the formula is valid under the given assumptions, False if it is not valid, and None if the validity cannot be determined. The options are directly passed to RCF.simplify.is_valid(), which is used internally.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> is_valid(z * ~z >= 0)
True
>>> is_valid(Re(z) > 0, assume=[z == 0])
False
>>> print(is_valid(z == 0))
None

Attention

The following functions are not intended to be used directly by the user. Instead, they are used internally by the functions simplify() and is_valid(). However, they might be useful for advanced users who want to reconstruct complex formulas.

Internal Representation and Simplify#

class logic1.theories.Complex.simplify.Options[source]#

Bases: Options

Options for the simplification process. Currently empty, but can be extended in the future. Implements the abstract class abc.simplify.Options.

class logic1.theories.Complex.simplify.InternalRepresentation[source]#

Bases: InternalRepresentation[AtomicFormula, Term, Variable, int | float | Fraction | mpq | complex]

Internal representation of a set of atomic formulas that are merged on extract(). Implements the abstract class abc.simplify.InternalRepresentation.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> rep = InternalRepresentation()
>>> _ = rep.add(And, [Re(z) == 0, Im(z) == 0])
>>> _ = rep.add(And, [z**2 == 1])
>>> atoms = rep.extract(And, InternalRepresentation())
>>> atoms.sort()
>>> atoms
[z == 0, z**2 - 1 == 0]

add(gand: type[And | Or], atoms: Iterable[AtomicFormula]) → RESTART[source]#: Implements the abstract method abc.simplify.InternalRepresentation.add().

extract(gand: type[And | Or], ref: Self) → list[AtomicFormula][source]#: Implements the abstract method abc.simplify.InternalRepresentation.extract().

next_(remove: Variable | None = None) → Self[source]#: Implements the abstract method abc.simplify.InternalRepresentation.next_().

class logic1.theories.Complex.simplify.Simplify[source]#

Bases: Simplify[AtomicFormula, Term, Variable, int | float | Fraction | mpq | complex, InternalRepresentation, Options]

Basic simplifier for merging pairs of atomic formulas using InternalRepresentation. Implements the abstract class abc.simplify.Simplify.

Simplification

Contents

Simplification#

User Interface#

Internal Representation and Simplify#