Type Members

1.  abstract class ColumnSolver extends AnyRef

   Abstract class for solving a conjunction of equations through column operations.

2.  class EquationConj extends EquationSet with SortedWithOrder[EquationConj]

   The class for representing conjunctions of equations, i.e., of systems of equations.

   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.

3.  abstract class EquationSet extends Formula with IndexedSeq[LinearCombination]
4.  class NegEquationConj extends EquationSet with SortedWithOrder[NegEquationConj]

   The class for representing disjunctions of equations (seen as conjunctions of negated equations)

5.  class ReduceWithEqs extends AnyRef

   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

6.  class ReduceWithNegEqs extends AnyRef