The Floating Point Arithmetic Validation Tool uses JavaScript to evaluate an Expression whose only operators are +, -, *, /, %, ^, =, >, <, >=, and <=. Since such JavaScript expressions can be inequalies and equations, they can evaluate to true or false in some cases. This tool marks the expression valid if and only if the JavaScript expression built from it evaluates to true.

The CAS Validation Tool uses Algebrite to evaluate whether an equation, inequality, or the statement isprime(n) is valid. It can be applied to a single Expression, and will mark it valid if and only if the expression is a valid Algebrite equation, inequality, or the statement isprime(n) where $n$ is an expression that evaluates to an integer, and the Algebrite check(expression) command returns 1.

The Classical Propositional Logic validation tool determines whether the propositional form of the sequent of a conclusion in an environment (not involving formulas or declarations) is a classical tautology.

This tool is installed with the tool name 'Classical Propositional Logic'. Thus, to use this tool to validate a conclusion, C, call Validation.setOptions and Validation.validate as follows:

Validation.setOptions(C,'tool','Classical Propositional Logic')
Validation.validate(C)

That will result in the validation results being stored in $C$ as an attribute.

The Intuitionistic Propositional Logic validation tool determines whether the propositional form of the sequent of a conclusion in an environment (not involving formulas or declarations) is intuitionistically valid in the fragment of propositional logic generated by implication and conjunction.

This tool is installed with the tool name 'Intuitionistic Propositional Logic'. Thus, to use this tool to validate a conclusion, C, call Validation.setOptions and Validation.validate as follows:

Validation.setOptions(C,'tool','Intuitionistic Propositional Logic')
Validation.validate(C)

That will result in the validation results being stored in $C$ as an attribute.