## Calling Sequence

## 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

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