Add an explicit theory axiom.
Add an explicit theory axiom. The action can specify a list of assumptions that are antecedents of the axiom and assumed to be present in a goal. Constants in the axiom will be replaced with universally quantified variables.
Add a formula to the handled proof goal.
Add a formula to the handled proof goal. This action does not support generation of proof certificates.
Record that values of the given constants can be reconstructed from the provided facts.
Split a proof goal into multiple sub-goals, and justify the split through an explicit theory axiom.
Split a proof goal into multiple sub-goals, and justify the split through an explicit theory axiom. The action can specify a list of assumptions that are antecedents of the axiom, but already assumed to be present in a goal. Constants in the axiom will be replaced with universally quantified variables.
Close the goal by invoking an explicit theory axiom.
Close the goal by invoking an explicit theory axiom. The action can specify a list of assumptions that are antecedents of the axiom and assumed to be present in a goal. Constants in the axiom will be replaced with universally quantified variables.
Remove some facts from the handled proof goal.
Schedule a task to be applied later on the goal.
Split a disequality fact into two inequalities.
Split a proof goal into multiple sub-goals.
Split a proof goal into multiple sub-goals. This action does not support generation of proof certificates.
A simple relevance filter to get rid of axioms that follow trivially from built-in arithmetic rules.
A simple relevance filter to get rid of axioms that follow trivially from built-in arithmetic rules. Such irrelevant axioms should not be added, since they might interfere with the built-in simplification rules, and sometimes lead to illformed proofs.