Abstract class for solving a conjunction of equations through column operations.
The class for representing conjunctions of equations, i.e., of systems of equations.
The class for representing disjunctions of equations (seen as conjunctions of negated equations)
Reduce a term (currently: a linear combination) by rewriting with equations.
Reduce a term (currently: a linear combination) by rewriting with equations. The equations have to be given in form of a mapping from atomic terms (constants or variables) to linear combinations
Reduce a term (currently: a linear combination) by rewriting with equations.
Reduce a term (currently: a linear combination) by rewriting with equations. The equations have to be given in form of a mapping from atomic terms (constants or variables) to linear combinations
The class for representing conjunctions of equations, i.e., of systems of equations. Systems of equations are always implicitly canonised and reduced by means of row operations, i.e., it is ensured that the leading terms of two equations are always distinct, and that no equation can be made smaller in the used
TermOrder
by adding multiples of other equations. This is not a complete method for deciding the satisfiability of a system, it is also necessary to perform column operations. Column operations are not applied implicitly, however.