ComputationLogger
Related Docs:
object ComputationLogger
| package terfor
Turn two complementary inequalities into an equation
Inference corresponding to a series of applications of the reduce rule: form the linear combination of a number of positive equations.
Inference corresponding to a series of applications of the reduce rule:
form the linear combination of a number of positive equations. The
given terms (apart from result) shall be primitive, with
a positive leading coefficient
Fourier-Motzkin Inference.
Fourier-Motzkin Inference. The given terms shall be primitive, and the result will be implicitly rounded
Compute the sum of multiple inequalities, and round the result afterwards.
Compute the sum of multiple inequalities, and round the result afterwards.
The argument ineqs might be stored and evaluated much later,
or not at all if the represented inference turns out to be unnecessary.
Given the two formulae t >= 0 and t != 0 (or,
similarly, t >= 0 and -t != 0), infer
the inequality t-1 >= 0.
Given the two formulae t >= 0 and t != 0 (or,
similarly, t >= 0 and -t != 0), infer
the inequality t-1 >= 0.
Instantiate a universally quantified formula with ground terms
Some other computation, that might in particular be performed by theory plug-ins.
Inference corresponding to a series of applications of the reduce rule to a
an inequality (reduction of positive equalities is
described using CombineEquationsInference).
Inference corresponding to a series of applications of the reduce rule to a
an inequality (reduction of positive equalities is
described using CombineEquationsInference).
Inference corresponding to a series of applications of the reduce rule to a
negated equation (reduction of positive equalities is
described using CombineEquationsInference).
Inference corresponding to a series of applications of the reduce rule to a
negated equation (reduction of positive equalities is
described using CombineEquationsInference).
Inference corresponding to a series of applications of the reduce rule to the arguments of a predicate literal.
Inference corresponding to a series of applications of the reduce rule to
the arguments of a predicate literal. This is essentially the same as the
reduceArithFormula, only that all of the arguments can be
reduced simultaneously
Apply the functional consistency axiom to derive that the results of two function applications (encoded as predicate atoms) must be the same.
Unify two predicates, producing a system of equations (in the succedent) that express the unification conditions: the predicate arguments are matched pair-wise
Convenient interface for combineEquations
Convenient interface for combineEquations
Convenient interface for combineInequalities
Convenient interface for combineInequalities
Convenient interface for otherComputation
Convenient interface for otherComputation
(Since version ) see corresponding Javadoc for more information.
Trait that can be used to track the computation taking place in systems of equations, inequalities, etc. This is used to produce proofs.