Complex

Quantifier Elimination

Quantifier elimination for the theory Complex.

Note

The function qe implements quantifier elimination for the theory of complex numbers. It takes a formula as input and returns an equivalent quantifier-free formula modulo optional assumptions.

>>> from logic1.firstorder import *
>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> qe(Ex(z, z**2 + 1 == 0))
T
>>> a = VV['a']
>>> qe(Ex(z, Re(z)**2 == a), assume=[Im(a) == 0])
a + ~a >= 0

Internally, quantifier elimination is performed by first converting the formula into RCF and then applying quantifier elimination qe for real closed fields.

User Interface

logic1.theories.Complex.qe.qe(formula: Formula[AtomicFormula, Term, Variable, int | float | Fraction | mpq | complex], assume: Iterable[AtomicFormula] = [], use_redlog: bool = False, **options) → Formula[AtomicFormula, Term, Variable, int | float | Fraction | mpq | complex]

Return a quantifier-free formula equivalent to the input formula.

Parameters:

• formula – The input formula to which quantifier elimination will be applied.

• assume – A list of atomic formulas that are assumed to hold. The return value is equivalent modulo those assumptions.

• use_redlog – If True, use RCF.redlog.qe() internally to perform real quantifier elimination. By default, RCF.qe.qe() is used.

• options – Additional keyword arguments to be passed to RCF.qe.qe() or RCF.redlog.qe().

>>> z = VV['z']
>>> phi = Ex(z, z**2 == -1)
>>> qe(phi)
T

RCF–Complex Conversion

Attention

The following functions are not intended to be used directly by the user. Instead, they are used internally by the function qe. However, they might be useful for advanced users who want to convert formulas and terms between the theory of complex numbers and the theory of real closed fields.

logic1.theories.Complex.qe.real_formula_to_rcf(formula: Formula[AtomicFormula, Term, Variable, int | float | Fraction | mpq | complex]) → Formula[AtomicFormula, Term, Variable, int]

Convert a real formula in the theory of complex numbers to an equivalent formula in the theory of real closed fields.

>>> z = VV['z']
>>> phi = All(z, z * ~z == 0)
>>> real_formula_to_rcf(phi)
All(z_re, All(z_im, z_im**2 + z_re**2 == 0))

logic1.theories.Complex.qe.real_normal_form(formula: Formula[AtomicFormula, Term, Variable, int | float | Fraction | mpq | complex]) → Formula[AtomicFormula, Term, Variable, int | float | Fraction | mpq | complex]

Convert all atoms in the formula into real normal form.

>>> z = VV['z']
>>> phi = Ex(z, z * ~z == 0)
>>> real_normal_form(phi)
Ex(z, And(z * ~z == 0, 0 == 0))

logic1.theories.Complex.qe.formula_to_rcf(formula: Formula[AtomicFormula, Term, Variable, int | float | Fraction | mpq | complex]) → Formula[AtomicFormula, Term, Variable, int]

Convert a formula in the theory of complex numbers to an equivalent formula in the theory of real closed fields.

>>> z = VV['z']
>>> phi = Ex(z, z**2 == -1)
>>> formula_to_rcf(phi)
Ex(z_re, Ex(z_im, And(-z_im**2 + z_re**2 + 1 == 0, 2*z_im*z_re == 0)))

logic1.theories.Complex.qe.term_to_complex(term: Term) → Term

Convert a RCF term to a complex term. The RCF term must be a polynomial in variables of the form *_re and *_im.

>>> z_re, z_im = RCF.VV.get('z_re', 'z_im')
>>> term = z_im**2 + z_re**2
>>> term_to_complex(term)
z * ~z

logic1.theories.Complex.qe.formula_to_complex(formula: Formula[AtomicFormula, Term, Variable, int]) → Formula[AtomicFormula, Term, Variable, int | float | Fraction | mpq | complex]

Convert a formula in the theory of real closed fields to an equivalent formula in the theory of complex numbers. Raise a ValueError if the RCF formula is quantified and or contains variables not of the form *_re and *_im.

>>> z_re, z_im = RCF.VV.get('z_re', 'z_im')
>>> phi = And(z_im**2 + z_re**2 == 0, 2*z_im*z_re == 0)
>>> formula_to_complex(phi)
And(z * ~z == 0, -1/2 * I * z**2 + 1/2 * I * (~z)**2 == 0)

class logic1.theories.Complex.qe.RCF_Evaluator

Bases: ArithmeticEvaluator[Term]

Visitor that evaluates a AST to a term in the theory of real closed fields. Raise a ValueError if the AST contains any complex-specific operations that cannot be evaluated. Implements the abstract class ArithmeticEvaluator.

>>> z = ast.Var('z')
>>> (ast.Re(z) + 1).accept(RCF_Evaluator())
z_re + 1
>>> (z + 1).accept(RCF_Evaluator())
Traceback (most recent call last):
...
ValueError: Cannot evaluate complex variable z in RCF

add(a: Term, b: Term) → Term

Return the sum of two RCF terms. Implements abstract method ArithmeticEvaluator.add().

>>> x, y = RCF.VV.get('x', 'y')
>>> RCF_Evaluator().add(x, y)
x + y

neg(a: Term) → Term

Return the negation of a RCF term. Implements the abstract method ArithmeticEvaluator.neg().

>>> x = RCF.VV['x']
>>> RCF_Evaluator().neg(x)
-x

mul(a: Term, b: Term) → Term

Return the product of two RCF terms. Implements the abstract method ArithmeticEvaluator.mul().

>>> x, y = RCF.VV.get('x', 'y')
>>> RCF_Evaluator().mul(x, y)
x*y

visit_rat(num: Rat) → Term

Return the RCF term corresponding to a rational number. Implements the abstract method ASTVisitor.visit_rat().

>>> RCF_Evaluator().visit_rat(ast.Rat(2))
2

visit_i(_: _I) → Term

Raise a ValueError since the imaginary unit cannot be evaluated in RCF. Implements the abstract method ASTVisitor.visit_i().

>>> RCF_Evaluator().visit_i(ast.I)
Traceback (most recent call last):
...
ValueError: Cannot evaluate imaginary unit in RCF

visit_var(var: Var) → Term

Raise a ValueError since complex variables cannot be evaluated in RCF. Implements the abstract method ASTVisitor.visit_var().

>>> z = ast.Var('z')
>>> RCF_Evaluator().visit_var(z)
Traceback (most recent call last):
...
ValueError: Cannot evaluate complex variable z in RCF

visit_conj(conj: Conj) → Term

Raise a ValueError since complex conjugation cannot be evaluated in RCF. Implements the abstract method ASTVisitor.visit_conj().

>>> z = ast.Var('z')
>>> RCF_Evaluator().visit_conj(z)
Traceback (most recent call last):
...
ValueError: Cannot evaluate complex conjugation in RCF

visit_re(re: Re) → Term

Return the RCF term corresponding to the real part of a complex variable. If the argument of re is not a variable, raise a ValueError. Implements the abstract method ASTVisitor.visit_re().

>>> z = ast.Var('z')
>>> RCF_Evaluator().visit_re(ast.Re(z))
z_re
>>> RCF_Evaluator().visit_re(ast.Re(z + 1))
Traceback (most recent call last):
...
ValueError: Cannot evaluate real part of non-variable term z + 1 in RCF

visit_im(im: Im) → Term

Return the RCF term corresponding to the imaginary part of a complex variable. If the argument of im is not a variable, raise a ValueError. Implements the abstract method ASTVisitor.visit_im().

>>> z = ast.Var('z')
>>> RCF_Evaluator().visit_im(ast.Im(z))
z_im
>>> RCF_Evaluator().visit_im(ast.Im(z + 1))
Traceback (most recent call last):
...
ValueError: Cannot evaluate imaginary part of non-variable term z + 1 in RCF