Variables, Terms, Atoms

Real Closed Fields

Variables, Terms, Atoms#

class logic1.theories.RCF.atomic.VariableSet[source]#

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[source]#: Implements abstract method firstorder.atomic.VariableSet.__getitem__().

fresh(suffix: str = '') → Variable[source]#: 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.

abstractmethod pop() → None[source]#
abstractmethod push() → None[source]#: 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.DEFINITE[source]#

Bases: Enum

Information whether a certain term has positive or negative definiteness properties; typically as a result of a heuristic test as in Term.is_definite().

NEGATIVE = 1#: The polynomial negative definite, i.e., negative for all real choices of variables.

NEGATIVE_SEMI = 2#: The polynomial negative semi-definite, i.e., non-positive for all real choices of variables.

NONE = 3#: None of the other cases holds..

POSITIVE = 4#: The polynomial positive definite, i.e., positive for all real choices of variables.

POSITIVE_SEMI = 5#: The polynomial positive semi-definite, i.e., non-negative for all real choices of variables.

ZERO = 6#: The polynomial is the zero polynomial.

class logic1.theories.RCF.atomic.Term[source]#

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

+, *, -, **, /
__add__(other: object) → Term[source]#
__mul__(other: object) → Term[source]#
__neg__() → Term[source]#
__pow__(other: object) → Term[source]#
__radd__(other: object) → Term[source]#
__rmul__(other: object) → Term[source]#
__rsub__(other: object) → Term[source]#
__sub__(other: object) → Term[source]#
__truediv__(other: object) → Term[source]#: Arithmetic operations on Terms are available as overloaded operators.

==, >=, >, <=, <, !=
__eq__(other: Term | int) → Eq[source]#
__ge__(other: Term | int) → Ge | Le[source]#
__gt__(other: Term | int) → Gt | Lt[source]#
__le__(other: Term | int) → Ge | Le[source]#
__lt__(other: Term | int) → Gt | Lt[source]#
__ne__(other: Term | int) → Ne[source]#: Construction of instances of Eq, Ge, Gt, Le, Lt, Ne is available via overloaded operators.

__iter__() → Iterator[tuple[mpq, Term]][source]#

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]
[(mpq(1,1), x^2), (mpq(2,1), x*y), (mpq(1,1), y^2), (mpq(4,1), x),
 (mpq(4,1), y), (mpq(4,1), 1)]

as_latex() → str[source]#

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[source]#

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() → mpq[source]#

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()
mpq(4,1)

content() → mpq[source]#

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()
mpq(2,1)

See also

MPolynomial.content()

degree(x: Variable) → int[source]#

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[source]#

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[mpq, dict[Term, int]][source]#

A polynomial factorization of this term.

Returns:: A pair (unit, D), where unit is a rational number, the keys of D are irreducible factors, and the corresponding values are their multiplicities. All irreducible factors are monic. Note that the return value is uniquely determined by this specification.

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

See also

MPolynomial_libsingular.factor()

is_constant() → bool[source]#: Return True if this term is constant.

See also

MPolynomial_libsingular.is_constant()

is_definite() → DEFINITE[source]#

A fast heuristic test for definitetess properties of this term. This is based on trivial square sum properties of coefficient signs and exponents.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> Term(0).is_definite()
<DEFINITE.ZERO: 6>
>>> f = x**2 + y**2
>>> f.is_definite()
<DEFINITE.POSITIVE_SEMI: 5>
>>> g = -x**2 - y**2 - 1
>>> g.is_definite()
<DEFINITE.NEGATIVE: 1>
>>> h = (x + y) ** 2
>>> h.is_definite()
<DEFINITE.NONE: 3>

is_zero() → bool[source]#: Return True if this term is a zero.

See also

MPolynomial_libsingular.is_zero()

lc() → mpq[source]#

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()
mpq(2,1)

See also

MPolynomial_libsingular.lc()

monomials() → list[Term][source]#

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][source]#

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)  # would yield (0, 2*x^2*y + x + 1) over ZZ
(2/3*x*y + 1/3, 1)

See also

MPolynomial_libsingular.quo_rem()

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

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()

sort_key() → SortKey[Self][source]#: A sort key suitable for ordering instances of this class. ImplementTerm(remainder)s the abstract method firstorder.atomic.Term.sort_key().

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

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][source]#: 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[source]#

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

fresh() → Variable[source]#: Returns a variable that has not been used so far. Implements abstract method firstorder.atomic.Variable.fresh().

class logic1.theories.RCF.atomic.AtomicFormula[source]#

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[source]#: 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[source]#: Returns True if this atomic formula should be sorted before or is equal to other. Implements abstract method firstorder.atomic.AtomicFormula.__le__().

__str__() → str[source]#: String representation of this atomic formula. Implements the abstract method firstorder.atomic.AtomicFormula.__str__().

as_latex() → str[source]#: Latex representation as a string. Implements the abstract method firstorder.atomic.AtomicFormula.as_latex().

bvars(quantified: frozenset[Variable] = frozenset({})) → Iterator[Variable][source]#: 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][source]#

classmethod converse(cls) → type[AtomicFormula][source]#

classmethod dual(cls) → type[AtomicFormula][source]#

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\).

fvars(quantified: frozenset[Variable] = frozenset({})) → Iterator[Variable][source]#: 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][source]#: Fast basic simplification. The result is equivalent to self. Implements the abstract method firstorder.atomic.AtomicFormula.simplify().

classmethod strict_part() → type[Gt | Lt][source]#

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 | mpq]) → Self[source]#: 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[source]#
class logic1.theories.RCF.atomic.Ge[source]#
class logic1.theories.RCF.atomic.Gt[source]#
class logic1.theories.RCF.atomic.Le[source]#
class logic1.theories.RCF.atomic.Lt[source]#
class logic1.theories.RCF.atomic.Ne[source]#: Bases: AtomicFormula

Variables, Terms, Atoms

Contents

Variables, Terms, Atoms#