Redlog Documentation Center

This new documentation in under construction. For functions not covered yet, please use the old documentation.

documentationgenericrlset

rlset – set current domain and autoload Redlog

Calling Sequence

rlset \((\,D\,)\)
rlset \((\,D\,,\ X\,)\)
rlset \((\,L\,)\)
rlset \((\,\,)\)

Arguments

\(D\) identifier
\(X\) additional domain-specific arguments
\(L\) list

Returns

\(L\) list

Description

Redlog works with first-order logic for fixed domains, where a domain specifies both a signature and a corresponding semantics.a rlset fixes the current domain \(D\) and returns the old one as a list \(L\) that can be used as an argument to rlset later on. When called without arguments the current domain is returned without modifying anything.

Initially, the domain is unset which does not admit any relevant computations. As a consequence, Redlog sessions typically start with a call to rlset, which autoloads the Redlog package making obsolete the load_package redlog; used with older versions of Redlog.

For a domain names there typically a long name and a short name plus an old name for backward compatibility. Some domains admit additional arguments \(X\). The following table collects the possible choices:

convenient name  \(\boldsymbol{D}\)   \(\boldsymbol{X}\)  signature (syntax) first-order theory (semantics)
quantified Boolean formulas boolean B ibalp \(=\), \(\sim\), \(\&\), \(\mid\), \(\rightarrow\), \(\leftarrow\), \(\leftrightarrow\); constants \(0\), \(1\) initial Boolean algebras
integers integers Z pasf \(=\), \(\neq\), \(<\), \(>\), \(\leq\), \(\geq\); \(-\), \(+\), \(\cdot\), constants from \(\mathbb Z\) first-order theory of the integers
real numbers reals R ofsf \(=\), \(\neq\), \(<\), \(>\), \(\leq\), \(\geq\); \(-\), \(+\), \(\cdot\), constants from \(\mathbb Z\) real closed fields
\(p\)-adic numbers padics dvfsf prime \(q>0\) \(=\), \(\neq\), \(\mid\), \(\parallel\), \(\sim\), \(\not\sim\); \(-\), \(+\), \(\cdot\), constants from \(\mathbb Z\) discretely valued fields with residue class field characteristic equal to \(q\)
prime \(q<0\) discretely valued fields with residue class field characteristic at most \(-q\)
0 or nothing \(=\), \(\neq\), \(\mid\), \(\parallel\), \(\sim\), \(\not\sim\); \(-\), \(+\), \(\cdot\), constants from \(\mathbb Z\cup\{p\}\) discretely valued fields with residue class field characteristic \(p\)
complex numbers complex C acfsf \(=\), \(\neq\); \(-\), \(+\), \(\cdot\), constants from \(\mathbb Z\) algebraically closed fields of characteristic 0
differential algebras differential dcfsf \(=\), \(\neq\); \(-\), \(+\), \(\cdot\), binary derivative \(d\), constants from \(\mathbb Z\) differentially closed fields
term algebras terms talp a sequence of pairs \(\{f,n\}\) introducing function symbols \(f\) of aritiy \(n\) \(=\), \(\neq\); function symbols specified in \(X\); \(\operatorname{inv}_{f,1}\), ..., \(\operatorname{inv}_{f,n}\) for each \(\{f,n\}\) in \(X\) The \(f\) introduced in \(X\) are free; \(\operatorname{inv}_{f,i}(t)=s\)  if \(t\) starts with \(f\) and the \(i\)-th argument of that \(f\) is \(s\); \(\operatorname{inv}_{f,i}(t)=t\)  else.
two-sided queues queues qqe another domain \(D\) two-sorted: (1) \(=\), \(\neq\); unary operators \(\operatorname{lhead}\), \(\operatorname{ltail}\), \(\operatorname{rhead}\), \(\operatorname{rtail}\); (2) the signature of the domain specified in \(X\) Currently, the only admissible choice for queue elements is real numbers via \(X={}\)ofsf.

The references below are the best matches for the various domains in the literature: [3] introduces our domain for Boolean quantified formulas; [2] gives a good background for our algorithms on the integers; [6] contains a lot of concrete computations with the real domain.

The work in [5] gave rise to the implementation of the \(p\)-adic domain. Note that all quantifier elimination methods are limited to the linear case such that the notions of \(p\)-adically closed or Henselian fields are not relevant here.

The complex domain has hardly been used in the literature so far. In the first place it implements a quantifier elimination procedure introduced in [8] and based on comprehensive bases. Note that the signature does not include and symbols for real part, imaginary part, or complex absolute value. For problems requiring any of these, one woud split variables into real and imaginary part, use \(i\) as a free variable, and apply real quantifier elimination.

Publications [1], [7], and [4] are the theoretical foundations for the domains for differential algebras, term algebras, and two-sided queues, respectively.

Examples

rlset boolean;
rlset R;
rlset(padics, -11);
rlset(terms, {zero, 0}, {one, 0}, {minus, 1}, {plus, 2});
rlset(queues, ofsf);

References

  1. A. Dolzmann and T. Sturm. Generalized constraint solving over differential algebras. Proc. CASC 2004. TU München, Germany, 2004.
  2. A. Lasaruk and T. Sturm. Weak quantifier elimination for the full linear theory of the integers. AAECC 18(6), 2007.
  3. A. Seidl and T. Sturm. Boolean quantification in a first-order context. Proc. CASC 2003. TU München, Germany, 2003.
  4. C. Straßer. Quantifier elimination for queues. Proc. RWCA 2006. Universität Basel, Switzerland, 2006.
  5. T. Sturm. Linear problems in valued fields. J. Symb. Comput. 30(2), 2000.
  6. T. Sturm and V. Weispfenning. Computational geometry problems in Redlog. Proc. ADG 2007. LNAI 1360, 1998.
  7. T. Sturm and V. Weispfenning. Quantifier elimination in term algebras. Proc. CASC 2002. TU München, Germany, 2002.
  8. V. Weispfenning. Comprehensive Gröner bases. J. Symb. Comput., 14(1), 1992.