Real Closed Fields

Variables, Terms, Atoms

class logic1.theories.RCF.atomic.VariableSet

Bases: VariableSet[Variable]

The infinite set of all variables belonging to the theory of Real Closed Fields. Variables are uniquely identified by their name, which is a str. This class is a singleton, whose single instance is assigned to VV.

See also

Final methods inherited from parent class:

• firstorder.atomic.VariableSet.get()

  – obtain several variables simultaneously

• firstorder.atomic.VariableSet.imp()

  – import variables into global namespace

__getitem__(index: str) → Variable

Implements abstract method firstorder.atomic.VariableSet.__getitem__().

fresh(suffix: str = '') → Variable

Return a fresh variable, by default from the sequence G0001, G0002, …, G9999, G10000, … This naming convention is inspired by Lisp’s gensym(). If the optional argument suffix is specified, the sequence G0001<suffix>, G0002<suffix>, … is used instead.

abstract pop() → None

abstract push() → None

Implement abstract methods logic1.firstorder.atomic.VariableSet.pop() and logic1.firstorder.atomic.VariableSet.push().

logic1.theories.RCF.atomic.VV = VariableSet()

The unique instance of VariableSet.

class logic1.theories.RCF.atomic.TSQ

Bases: Enum

Information whether a certain term is has a trivial square sum property.

See also

Term.is_definite()

NONE = 1

None of the other cases holds..

STRICT = 2

All other integer coefficients, including the absolute summand, are strictly positive. All exponents are even. This is sufficient for a term to be positive definite, i.e., positive for all real choices of variables.

WEAK = 3

The absolute summand is zero. All other integer coefficients are strictly positive. All exponents are even. This is sufficient for a term to be positive semi-definite, i.e., non-negative for all real choices of variables.

class logic1.theories.RCF.atomic.Term

Bases: Term[Term, Variable, int]

+, *, -, **, /

__add__(other: object) → Term

__mul__(other: object) → Term

__neg__() → Term

__pow__(other: object) → Term

__radd__(other: object) → Term

__rmul__(other: object) → Term

__rsub__(other: object) → Term

__sub__(other: object) → Term

__truediv__(other: object) → Term

Arithmetic operations on Terms are available as overloaded operators.

==, >=, >, <=, <, !=

__eq__(other: Term | int) → Eq

__ge__(other: Term | int) → Ge | Le

__gt__(other: Term | int) → Gt | Lt

__le__(other: Term | int) → Ge | Le

__lt__(other: Term | int) → Gt | Lt

__ne__(other: Term | int) → Ne

Construction of instances of Eq, Ge, Gt, Le, Lt, Ne is available via overloaded operators.

__iter__() → Iterator[tuple[int, Term]]

Iterate over the polynomial representation of the term, yielding pairs of coefficients and power products.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2
>>> [(abs(coef), power_product) for coef, power_product in t]
[(1, x^2), (2, x*y), (1, y^2), (4, x), (4, y), (4, 1)]

as_latex() → str

LaTeX representation as a string. Implements the abstract method firstorder.atomic.Term.as_latex().

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2
>>> t.as_latex()
'x^{2} - 2 x y + y^{2} + 4 x - 4 y + 4'

coefficient(degrees: dict[Variable, int]) → Term

Return the coefficient of the variables with the degrees specified in the python dictionary degrees.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2
>>> t.coefficient({x: 1, y: 1})
-2
>>> t.coefficient({x: 1})
-2*y + 4

See also

MPolynomial_libsingular.coefficient()

constant_coefficient() → int

Return the constant coefficient of this term.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2
>>> t.constant_coefficient()
4

See also

MPolynomial_libsingular.constant_coefficient()

content() → int

Return the content of this term, which is defined as the gcd of its integer coefficients.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2 - (x**2 + y**2)
>>> t.content()
2

See also

MPolynomial.content()

degree(x: Variable) → int

Return the degree in x of this term.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2
>>> t.degree(y)
2

See also

MPolynomial_libsingular.degree()

derivative(x: Variable, n: int = 1) → Term

The n-th derivative of this term, with respect to x.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2
>>> t.derivative(x)
2*x - 2*y + 4

See also

MPolynomial.derivative()

factor() → tuple[Term, Term, dict[Term, int]]

Return the factorization of this term.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = x**2 - y**2
>>> t.factor()
(1, 1, {x - y: 1, x + y: 1})

See also

MPolynomial_libsingular.factor()

is_constant() → bool

Return True if this term is constant.

See also

MPolynomial_libsingular.is_constant()

is_definite() → TSQ

A fast heuristic test whether this term is positive or non-negative for all real choices of variables.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> f = x**2 + y**2
>>> f.is_definite()
<TSQ.WEAK: 3>
>>> g = x**2 + y**2 + 1
>>> g.is_definite()
<TSQ.STRICT: 2>
>>> h = (x + y) ** 2
>>> h.is_definite()
<TSQ.NONE: 1>

is_zero() → bool

Return True if this term is a zero.

See also

MPolynomial_libsingular.is_zero()

lc() → int

Leading coefficient of this term with respect to the degree lexicographical term order deglex.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> f = 2*x*y**2 + 3*x**2 + 1
>>> f.lc()
2

See also

MPolynomial_libsingular.lc()

monomials() → list[Term]

List of monomials of this term. A monomial is defined here as a summand of a polynomial without the coefficient.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2
>>> t.monomials()
[x^2, x*y, y^2, x, y, 1]

See also

MPolynomial_libsingular.monomials()

quo_rem(other: Term) → tuple[Term, Term]

Quotient and remainder of this term and other.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> f = 2*y*x**2 + x + 1
>>> f.quo_rem(x)
(2*x*y + 1, 1)
>>> f.quo_rem(y)
(2*x^2, x + 1)
>>> f.quo_rem(3*x)
(0, 2*x^2*y + x + 1)

See also

MPolynomial_libsingular.quo_rem()

pseudo_quo_rem(other: Term, x: Variable) → tuple[Term, Term]

Pseudo quotient and remainder of this term and other, both as univariate polynomials in x with polynomial coefficients in all other variables.

>>> a, b, c, x = VV.get('a', 'b', 'c', 'x')
>>> f = a * x**2 + b*x + c
>>> g = c * x + b
>>> q, r = f.pseudo_quo_rem(g, x); q, r
(a*c*x - a*b + b*c, a*b^2 - b^2*c + c^3)
>>> assert c**(2 - 1 + 1) * f == q * g + r

See also

Polynomial.pseudo_quo_rem()

static sort_key(term: Term) → MPolynomial_libsingular

A sort key suitable for ordering instances of this class. Implements the abstract method firstorder.atomic.Term.sort_key().

subs(d: Mapping[Variable, Term | int]) → Term

Simultaneous substitution of terms for variables.

>>> from logic1.theories.RCF import VV
>>> x, y, z = VV.get('x', 'y', 'z')
>>> f = 2*y*x**2 + x + 1
>>> f.subs({x: y, y: 2*z})
4*y^2*z + y + 1

See also

MPolynomial_libsingular.subs()

vars() → Iterator[Variable]

An iterator that yields each variable of this term once. Implements the abstract method firstorder.atomic.Term.vars().

See also

MPolynomial_libsingular.variables()

class logic1.theories.RCF.atomic.Variable

Bases: Term, Variable[Variable, int]

fresh() → Variable

Returns a variable that has not been used so far. Implements abstract method firstorder.atomic.Variable.fresh().

class logic1.theories.RCF.atomic.AtomicFormula

Bases: AtomicFormula[AtomicFormula, Term, Variable, int]

property lhs: Term

property rhs: Term

The left hand side term and the right hand side term of an atomic formula.

__bool__() → bool

In boolean contexts atomic formulas are evaluated via corresponding comparisons with respect to the degree lexicographical term order deglex. In particular, comparisons between terms representing integers follow the natural order.

__le__(other: Formula[AtomicFormula, Term, Variable, int]) → bool

Returns True if this atomic formula should be sorted before or is equal to other. Implements abstract method firstorder.atomic.AtomicFormula.__le__().

__str__() → str

String representation of this atomic formula. Implements the abstract method firstorder.atomic.AtomicFormula.__str__().

as_latex() → str

Latex representation as a string. Implements the abstract method firstorder.atomic.AtomicFormula.as_latex().

bvars(quantified: frozenset[Variable] = frozenset({})) → Iterator[Variable]

Iterate over occurrences of variables that are elements of quantified. Yield each such variable once for each term that it occurs in. Implements the abstract method firstorder.atomic.AtomicFormula.bvars().

classmethod complement(cls) → type[AtomicFormula]

classmethod converse(cls) → type[AtomicFormula]

classmethod dual(cls) → type[AtomicFormula]

Complement relation, converse relation, and dual relation. complement() implements the abstract method firstorder.atomic.AtomicFormula.complement().

	Eq	Ne	Le	Ge	Lt	Gt
complement()	Ne	Eq	Gt	Lt	Ge	Le
converse()	Eq	Ne	Ge	Le	Gt	Lt
dual()	Ne	Eq	Lt	Gt	Le	Ge

Mathematical definitions

Let \(\varrho \subseteq A^n\) be an \(n\)-ary relation. Then the complement relation is defined as

\[\overline{\varrho} = A^n \setminus \varrho.\]

It follows that \(\overline{\varrho}(a_1, \dots, a_n)\) is equivalent to \(\lnot \varrho(a_1, \dots, a_n)\), which is an important property for Logic1.

If \(\varrho\) is binary, then the converse relation is defined as

\[\varrho^{-1} = \{\,(y, x) \in A^2 \mid (x, y) \in \varrho\,\}.\]

In other words, the converse swaps sides. It is the inverse with respect to composition, i.e., \(\varrho \circ \varrho^{-1} = \varrho^{-1} \circ \varrho = \Delta_A\). The diagonal \(\Delta_A = \{\,(x, y) \in A^2 \mid x = y\,\}\) is equality on \(A\).

Finally, the dual relation is defined as

\[\varrho^d = \overline{\varrho^{-1}},\]

which generally equals \((\overline{\varrho})^{-1}\). For our relations here, dualization amounts to turning strict relations into weak relations, and vice versa.

Each of these transformations of relations is involutive in the sense that \(\overline{\overline{\varrho}} = (\varrho^{-1})^{-1} = (\varrho^d)^d = \varrho\).

See also

Inherited method firstorder.atomic.AtomicFormula.to_complement()

fvars(quantified: frozenset[Variable] = frozenset({})) → Iterator[Variable]

Iterate over occurrences of variables that are not elements of quantified. Yield each such variable once for each term that it occurs in. Implements the abstract method firstorder.atomic.AtomicFormula.fvars().

simplify() → Formula[AtomicFormula, Term, Variable, int]

Fast basic simplification. The result is equivalent to self. Implements the abstract method firstorder.atomic.AtomicFormula.simplify().

classmethod strict_part() → type[Gt | Lt]

The strict part of a binary relation is the relation without the diagonal. Raises NotImplementedError for Eq and Ne.

	Le	Ge	Lt	Gt
strict_part()	Lt	Gt	Lt	Gt

subs(sigma: Mapping[Variable, Term | int]) → Self

Formal simultaneous term substitution into the two argument terms of the atomic formula. Implements the abstract method firstorder.atomic.AtomicFormula.subs().

class logic1.theories.RCF.atomic.Eq

class logic1.theories.RCF.atomic.Ge

class logic1.theories.RCF.atomic.Gt

class logic1.theories.RCF.atomic.Le

class logic1.theories.RCF.atomic.Lt

class logic1.theories.RCF.atomic.Ne

Bases: AtomicFormula