Real Closed Fields

Variables, Terms, Atoms

There is an infinite set RCF.VV of all RCF variables, which is an instance of the class VariableSet. The variables obtained from VV are instances of the class Variable, which is a subclass of Term. Larger terms can be constructed from variables and numbers using ring arithmetic +, *, -, **, / implemented in Term.

There is a class AtomicFormula with subclasses Eq, Ne, Le, Ge, Lt, Gt. Atoms are obtained as instances of these subclasses either using the class names as constructors, or using the corresponding operators ==, !=, <=, >=, < > overloaded in the class Term. The following diagram, which has no rigorous formal semantics, illustrates this.

Some examples can be found on the landing page of this section.

The Set of All Variables

class logic1.theories.RCF.term.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.

The use of VV for the construction of terms, atoms, and formulas is described in the introduction of the section Real Closed Fields.

See also

Final methods inherited from the parent class:

• firstorder.term.VariableSet.get()

  – obtain several variables simultaneously

• firstorder.term.VariableSet.imp()

  – import variables into global namespace

property stack: list[MPolynomialRing_libsingular]

Implements the abstract property firstorder.term.VariableSet.stack.

__getitem__(index: str) → Variable

Implements the abstract method firstorder.term.VariableSet.__getitem__().

>>> from logic1.theories.RCF import VV
>>> isinstance(VV, VariableSet)
True
>>> x = VV['x']
>>> isinstance(x, Variable)
True

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.

>>> from logic1.theories.RCF import VV
>>> VV.fresh('_demo')
G0001_demo
>>> VV.fresh('_demo')
G0002_demo

pop() → None

push() → None

Implements the abstract methods logic1.firstorder.term.VariableSet.pop() and push().

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

The unique instance of VariableSet.

Terms and Variables

class logic1.theories.RCF.term.Term

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

+, *, -, **, /

__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 these 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 these overloaded operators.

__init__(self, arg: float | int | Fraction | mpq | Integer | Rational | MPolynomial[Rational] | UPolynomial) → None

Construct a Term from float, int, Fraction, or mpq. Arguments of the following types are private and should not be used outside of this module: Integer, Rational, MPolynomial[Rational], UPolynomial.

>>> from logic1.theories.RCF import Term
>>> Term(0.1 + 0.2)
415716888680356/1385722962267853
>>> Term(42)
42
>>> Term(Fraction(1, 42))
1/42
>>> Term(mpq(1, 42))
1/42

Attention

Python division of integers yields a float, which can cause precision issues:

>>> Term(1/10 + 2/10)
415716888680356/1385722962267853

In contrast:

>>> Term(mpq(1, 10) + mpq(2, 10))
3/10
>>> Term(Fraction(1, 10) + Fraction(2, 10))
3/10

__iter__() → Iterator[tuple[mpq, 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]
[(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)]

__str__()

Return the mathematical string representation of this term.

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

as_constant() → mpq

Return this term as an mpq. Raise ValueError if this term is not constant.

>>> from logic1.theories.RCF import VV
>>> x = VV['x']
>>> t = x + mpq(1, 2) - x
>>> t
1/2
>>> isinstance(t, Term)
True
>>> isinstance(t, mpq)
False
>>> c = t.as_constant()
>>> c
mpq(1,2)
>>> isinstance(c, mpq)
True

See also

Term.is_constant()

as_latex() → str

LaTeX representation as a string. Implements the abstract method firstorder.term.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'

as_variable() → Variable

Return this term as an instance of the subclass Variable. Raise ValueError if this term is not a variable.

>>> from logic1.theories.RCF import VV
>>> x = VV['x']
>>> t = x + 1 - 1
>>> t
x
>>> isinstance(t, Term)
True
>>> isinstance(t, Variable)
False
>>> v = t.as_variable()
>>> v
x
>>> isinstance(v, Variable)
True

See also

Term.is_variable()

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

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)

See also

MPolynomial_libsingular.constant_coefficient()

content() → mpq

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

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

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.

>>> x, y = VV.get('x', 'y')
>>> t = -x**2 + y**2
>>> t.factor() == (mpq(-1,1), {x - y: 1, x + y: 1})
True

It is noteworthy that Sage factorization over QQ does not always yield monic factors.

>>> a, b = VV.get('a', 'b')
>>> t = 2*a**2 + 4*a*b + 2*b**2 - 1
>>> t.factor() == (mpq(2,1), {a**2 + 2*a*b + b**2 - 1/2: 1})
True
>>> sage_factorization = t.poly.factor()
>>> sage_factorization.unit(), list(sage_factorization)
(1, [(2*a^2 + 4*a*b + 2*b^2 - 1, 1)])

See also

MPolynomial_libsingular.factor()

is_constant() → bool

Return True if this term is constant from a mathematical perspective.

>>> from logic1.theories.RCF import VV
>>> x = VV['x']
>>> t = x + mpq(1, 2) - x
>>> t
1/2
>>> isinstance(t, mpq)
False
>>> t.is_constant()
True

See also

• as_constant()

• MPolynomial_libsingular.is_constant()

is_definite(assume: Mapping[Variable, DEFINITE] = {}) → DEFINITE

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

>>> x, y = VV.get('x', 'y')
>>> print(Term(0).is_definite())
DEFINITE.ZERO
>>> f = x**2 + y**2
>>> print(f.is_definite())
DEFINITE.POSITIVE_SEMI
>>> g = -x**2 - y**2 - 1
>>> print(g.is_definite())
DEFINITE.NEGATIVE
>>> h = (x - y) ** 2
>>> print(h.is_definite())
DEFINITE.UNKNOWN
>>> print(h.is_definite(assume={x: DEFINITE.POSITIVE, y: DEFINITE.NEGATIVE}))
DEFINITE.POSITIVE
>>> print(h.is_definite(assume={x: DEFINITE.NEGATIVE_SEMI, y: DEFINITE.POSITIVE_SEMI}))
DEFINITE.POSITIVE_SEMI

is_monomial() → bool

Return True if this term is a monomial.

is_variable() → bool

Return True if this term is a variable from a mathematical perspective.

>>> from logic1.theories.RCF import VV
>>> x = VV['x']
>>> t = x + 1 - 1
>>> isinstance(t, Term)
True
>>> isinstance(t, Variable)
False
>>> t.is_variable()
True

See also

as_variable()

is_weakly_parametric_linear(X: Container[Variable]) → bool

Return True if this Term can be written as \(a_1 x_1 + ... + a_n x_n + r\) such that \(a_1, ..., a_n \in \mathbb{Q}\), \(x_1, ..., x_n \in X\), and \(r\) is a polynomial over \(\mathbb{Q}\) that does not contain any variable from \(X\).

>>> a, b, x, y = VV.get('a', 'b', 'x', 'y')
>>> term = 2 * x - 3 * y + 4 * a**2 + 5 * a * b
>>> term.is_weakly_parametric_linear({x, y})
True
>>> term.is_weakly_parametric_linear({a})
False
>>> term.is_weakly_parametric_linear({b})
False

is_zero() → bool

Return True if this term is zero.

>>> from logic1.theories.RCF import VV
>>> x = VV['x']
>>> t = x - x
>>> t
0
>>> isinstance(t, Term)
True
>>> isinstance(t, int)
False
>>> t.is_zero()
True

See also

MPolynomial_libsingular.is_zero()

lc() → mpq

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

monomial_coefficient(mon: Term) → mpq

Return the coefficient in the base ring of the monomial mon in self, where mon must have the same parent as self. Raise ValueError if mon is not a monomial.

See also

MPolynomial_libsingular.monomial_coefficient()

monomials() → list[Term]

Return a list of all 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()

normalize() → Term

Divide this term by its leading coefficient, so that the result is monic.

primitive_part(positive: bool = False) → Term

Return the primitive part of this term. This is self divided by its (positive) content, so that self.content() * self.primitive_part() == self. If positive is True, the result is normalized to have a positive leading coefficient.

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

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

See also

MPolynomial_libsingular.quo_rem()

reduce(G: Iterable[Term]) → Term

Reduce self modulo G. The output is a polynomial r such that self - r is in the ideal generated by G, and no monomial of r is divisible by the leading monomial of any polynomial in G. The result is canonical if G is a Gröbner basis.

The elements of G must be coercible to the parent of self. Otherwise, a TypeError is raised.

See also

MPolynomial_libsingular.reduce()

sort_key() → SortKey[Self]

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

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

Simultaneous substitution of terms for variables.

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

See also

MPolynomial_libsingular.subs()

subs_linear_solution(x: Variable, minimal_polynomial: Term) → Term

Substitute the solution of the weakly parametric linear polynomial minimal_polynomial into this weakly parametric linear polynomial.

>>> from logic1.theories.RCF import VV
>>> a, b, x = VV.get('a', 'b', 'x')
>>> (2 * x + a).subs_linear_solution(x, 5 * x + b)
a - 2/5*b

It is asserted that both polynomials are weakly parametric linear in x, but no exception is raised if this is not the case.

summands() → Iterator[tuple[dict[Variable, int], mpq]]

Iterate over the summands of this term yielding pairs of monomials represented as dictionaries and coefficients.

>>> from logic1.theories.RCF import VV
>>> a, b, c = VV.get('a', 'b', 'c')
>>> f = a*c**3 + a**2*b + 2*b**4
>>> list(f.summands())
[({a: 1, c: 3}, mpq(1,1)), ({b: 4}, mpq(2,1)), ({a: 2, b: 1}, mpq(1,1))]

See also

MPolynomial_libsingular.iterator_exp_coeff()

vars() → Iterator[Variable]

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

See also

MPolynomial_libsingular.variables()

class logic1.theories.RCF.term.Variable

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

fresh() → Variable

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

logic1.theories.RCF.term.term_sage.τ = ~τ

A type variable denoting a type of terms with upper bound Term.

Support Classes for Terms

class logic1.theories.RCF.term.DEFINITE

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

UNKNOWN = 1

Heuristic tests could not derive that any the other cases holds.

ZERO = 2

The polynomial is the zero polynomial.

POSITIVE = 3

The polynomial positive definite, i.e., positive for all real choices of variables.

POSITIVE_SEMI = 4

The polynomial positive semi-definite, i.e., non-negative for all real choices of variables.

NEGATIVE = 5

The polynomial negative definite, i.e., negative for all real choices of variables.

NEGATIVE_SEMI = 6

The polynomial negative semi-definite, i.e., non-positive for all real choices of variables.

static add(x: DEFINITE, y: DEFINITE) → DEFINITE

Compute DEFINITE of a sum from DEFINITE of the summands.

>>> l = list(DEFINITE)

>>> for x in l:
...     for y in l:
...             print(f'{x.name} + {y.name} = {DEFINITE.add(x,y).name}')
...
UNKNOWN + UNKNOWN = UNKNOWN
UNKNOWN + ZERO = UNKNOWN
UNKNOWN + POSITIVE = UNKNOWN
UNKNOWN + POSITIVE_SEMI = UNKNOWN
UNKNOWN + NEGATIVE = UNKNOWN
UNKNOWN + NEGATIVE_SEMI = UNKNOWN
ZERO + UNKNOWN = UNKNOWN
ZERO + ZERO = ZERO
ZERO + POSITIVE = POSITIVE
ZERO + POSITIVE_SEMI = POSITIVE_SEMI
ZERO + NEGATIVE = NEGATIVE
ZERO + NEGATIVE_SEMI = NEGATIVE_SEMI
POSITIVE + UNKNOWN = UNKNOWN
POSITIVE + ZERO = POSITIVE
POSITIVE + POSITIVE = POSITIVE
POSITIVE + POSITIVE_SEMI = POSITIVE
POSITIVE + NEGATIVE = UNKNOWN
POSITIVE + NEGATIVE_SEMI = UNKNOWN
POSITIVE_SEMI + UNKNOWN = UNKNOWN
POSITIVE_SEMI + ZERO = POSITIVE_SEMI
POSITIVE_SEMI + POSITIVE = POSITIVE
POSITIVE_SEMI + POSITIVE_SEMI = POSITIVE_SEMI
POSITIVE_SEMI + NEGATIVE = UNKNOWN
POSITIVE_SEMI + NEGATIVE_SEMI = UNKNOWN
NEGATIVE + UNKNOWN = UNKNOWN
NEGATIVE + ZERO = NEGATIVE
NEGATIVE + POSITIVE = UNKNOWN
NEGATIVE + POSITIVE_SEMI = UNKNOWN
NEGATIVE + NEGATIVE = NEGATIVE
NEGATIVE + NEGATIVE_SEMI = NEGATIVE
NEGATIVE_SEMI + UNKNOWN = UNKNOWN
NEGATIVE_SEMI + ZERO = NEGATIVE_SEMI
NEGATIVE_SEMI + POSITIVE = UNKNOWN
NEGATIVE_SEMI + POSITIVE_SEMI = UNKNOWN
NEGATIVE_SEMI + NEGATIVE = NEGATIVE
NEGATIVE_SEMI + NEGATIVE_SEMI = NEGATIVE_SEMI

This addition is commutative:

>>> all(DEFINITE.add(x, y) is DEFINITE.add(y, x) for x in l for y in l)
True

DEFINITE.ZERO is a (unique) neutral element:

>>> all(DEFINITE.add(x, DEFINITE.ZERO) is x for x in l)
True

static from_constant(q: int | mpq | Rational) → DEFINITE

Compute DEFINITE of a number.

>>> print(DEFINITE.from_constant(mpq(42)))
DEFINITE.POSITIVE

>>> print(DEFINITE.from_constant(mpq(-4711)))
DEFINITE.NEGATIVE

>>> print(DEFINITE.from_constant(mpq(0)))
DEFINITE.ZERO

static mul(x: DEFINITE, y: DEFINITE) → DEFINITE

Compute DEFINITE of a product from DEFINITE of the factors.

>>> l = list(DEFINITE)

The multiplication table:

>>> for x in l:
...     for y in l:
...             print(f'{x.name} * {y.name} = {DEFINITE.mul(x,y).name}')
...
UNKNOWN * UNKNOWN = UNKNOWN
UNKNOWN * ZERO = ZERO
UNKNOWN * POSITIVE = UNKNOWN
UNKNOWN * POSITIVE_SEMI = UNKNOWN
UNKNOWN * NEGATIVE = UNKNOWN
UNKNOWN * NEGATIVE_SEMI = UNKNOWN
ZERO * UNKNOWN = ZERO
ZERO * ZERO = ZERO
ZERO * POSITIVE = ZERO
ZERO * POSITIVE_SEMI = ZERO
ZERO * NEGATIVE = ZERO
ZERO * NEGATIVE_SEMI = ZERO
POSITIVE * UNKNOWN = UNKNOWN
POSITIVE * ZERO = ZERO
POSITIVE * POSITIVE = POSITIVE
POSITIVE * POSITIVE_SEMI = POSITIVE_SEMI
POSITIVE * NEGATIVE = NEGATIVE
POSITIVE * NEGATIVE_SEMI = NEGATIVE_SEMI
POSITIVE_SEMI * UNKNOWN = UNKNOWN
POSITIVE_SEMI * ZERO = ZERO
POSITIVE_SEMI * POSITIVE = POSITIVE_SEMI
POSITIVE_SEMI * POSITIVE_SEMI = POSITIVE_SEMI
POSITIVE_SEMI * NEGATIVE = NEGATIVE_SEMI
POSITIVE_SEMI * NEGATIVE_SEMI = NEGATIVE_SEMI
NEGATIVE * UNKNOWN = UNKNOWN
NEGATIVE * ZERO = ZERO
NEGATIVE * POSITIVE = NEGATIVE
NEGATIVE * POSITIVE_SEMI = NEGATIVE_SEMI
NEGATIVE * NEGATIVE = POSITIVE
NEGATIVE * NEGATIVE_SEMI = POSITIVE_SEMI
NEGATIVE_SEMI * UNKNOWN = UNKNOWN
NEGATIVE_SEMI * ZERO = ZERO
NEGATIVE_SEMI * POSITIVE = NEGATIVE_SEMI
NEGATIVE_SEMI * POSITIVE_SEMI = NEGATIVE_SEMI
NEGATIVE_SEMI * NEGATIVE = POSITIVE_SEMI
NEGATIVE_SEMI * NEGATIVE_SEMI = POSITIVE_SEMI

This multiplication is commutative:

>>> all(DEFINITE.mul(x, y) is DEFINITE.mul(y, x) for x in l for y in l)
True

DEFINITE.POSITIVE is a (unique) neutral element:

>>> all(DEFINITE.mul(x, DEFINITE.POSITIVE) is x for x in l)
True

static square(x: DEFINITE) → DEFINITE

Compute DEFINITE of a square.

class logic1.theories.RCF.term.SortKey

Bases: Generic[τ]

Sort key for comparing terms.

>>> x = VV['x']
>>> SortKey(x) < SortKey(x + 1)
True

Atoms

class logic1.theories.RCF.atomic.AtomicFormula

Bases: AtomicFormula[logic1.theories.RCF.atomic.AtomicFormula, logic1.theories.RCF.term.Term, logic1.theories.RCF.term.Variable, int]

Base class for atomic formulas over real closed fields. The class is the common parent of Eq, Ne, Le, Ge, Lt, and Gt. It is not intended to be instantiated directly. Use one of the concrete relation classes instead.

property lhs: Term

property rhs: Term

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

__bool__() → bool

Evaluation of this atomic formula in a Boolean context.

In a Boolean context, atomic formulas are evaluated by comparing the left and right hand side terms using degree lexicographical term order. In particular, comparisons between terms representing integers follow the natural order.

__eq__(other: object) → bool

Return whether this atomic formula is equal to other.

Two atomic formulas are equal if they have the same relation and the sort keys of their corresponding left- and right-hand side terms are equal.

__le__(other: Formula) → bool

Return whether this atomic formula precedes or equals other in order.

Implements the abstract method firstorder.atomic.AtomicFormula.__le__().

Atomic formulas are ordered lexicographically by the sort keys of their left-hand and right-hand terms, followed by the ordering Eq < Ne < Le < Lt < Ge < Gt. Non-atomic formulas are considered greater than atomic formulas.

__str__() → str

Return the mathematical string representation of this atomic formula.

Implements the abstract method firstorder.atomic.AtomicFormula.__str__().

The relation symbol is written infix, using the usual ASCII operators '==', '!=', '<=', '>=', '<', and '>'. The representation of the left and right hand side terms is delegated to Term.__str__.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> atom = (x - y + 2) ** 2 >= 0
>>> str(atom)
'x^2 - 2*x*y + y^2 + 4*x - 4*y + 4 >= 0'

as_latex() → str

Return the LaTeX representation of this atomic formula.

Implements the abstract method firstorder.atomic.AtomicFormula.as_latex().

The relation symbol is rendered infix as '=', '\neq', '\leq', '\geq', '<', and '>'. The representation of the left and right hand side terms is delegated to Term.as_latex.

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

See also

firstorder.formula.Formula.as_latex()

LaTeX representation of first-order formulas

as_redlog() → str

Return the Redlog representation of this atomic formula.

Overloads the method firstorder.atomic.AtomicFormula.as_redlog(), which raises NotImplementedError.

Returns the Redlog representation of the atomic formula in parentheses.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> atom = (x - y + 2) ** 2 != 0
>>> atom.as_redlog()
'(x**2 - 2*x*y + y**2 + 4*x - 4*y + 4 <> 0)'

See also

firstorder.formula.Formula.as_redlog()

Redlog representation of first-order formulas

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

The bound variables of this atomic formula.

Implements the abstract method firstorder.atomic.AtomicFormula.bvars().

For each variable occurring in either term, yield it once for each term in which it occurs, provided that the variable belongs to quantified.

See also

fvars()

The free variables of this atomic formula.

firstorder.formula.Formula.bvars()

An iterator over all bound occurrences of variables in a first-order formula

classmethod complement() → type[AtomicFormula]

classmethod converse() → type[AtomicFormula]

classmethod dual() → type[AtomicFormula]

Return the complement relation, converse relation, dual relation of this subclass of AtomicFormula.

complement() implements the abstract method firstorder.atomic.AtomicFormula.complement().

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

This yields the following table for RCF:

	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

See also

Inherited method firstorder.atomic.AtomicFormula.to_complement()

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

The free variables of this atomic formula.

Implements the abstract method firstorder.atomic.AtomicFormula.fvars().

For each variable occurring in either term, yield it once for each term in which it occurs, provided that the variable does not belong to quantified.

See also

bvars()

The bound variables of this atomic formula.

firstorder.formula.Formula.fvars()

An iterator over all free occurrences of variables in a first-order formula

simplify() → Formula

Return a simplified equivalent of the atomic formula, using basic simplification rules.

Implements the abstract method firstorder.atomic.AtomicFormula.simplify().

If the difference between the left and right hand side terms of the input is constant, T or F is returned. Otherwise an AtomicFormula is returned which has the following properties:

1. The right hand side term is 0.

2. The left hand side term is not constant and its leading coefficient is non-negative.

See also

firstorder.formula.Formula.simplify()

Basic simplification of formulas, which uses this method for atomic formulas.

RCF.simplify.simplify()

More powerful simplification of formulas.

classmethod strict_part() → type[Gt | Lt]

Return the strict part of this subclass of AtomicFormula.

Raise NotImplementedError if this class is not an inequality.

Otherwise, the strict part is defined as the relation without the diagonal:

	Le	Ge	Lt	Gt
strict_part()	Lt	Gt	Lt	Gt

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

Return the atomic formula obtained from this atomic formula by simultaneous term substitution.

Implements the abstract method firstorder.atomic.AtomicFormula.subs().

The substitution sigma is applied independently and simultaneously to the left- and right-hand side terms.

See also

firstorder.formula.Formula.subs()

Simultaneous substitution of terms for variables in first-order formulas

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

See also

Term.__eq__, Term.__ge__, Term.__gt__, Term.__le__, Term.__lt__, Term.__ne__

for constructing instances of these classes using the corresponding infix operators ==, >=, >, <=, <, !=.