Plugin

Type Members

1. sealed abstract class Action extends AnyRef

   

2. case class AddAxiom(assumptions: Seq[Formula], axiom: Conjunction, theory: Theory) extends Action with Product with Serializable

   

   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.

3. case class AddFormula(formula: Conjunction) extends Action with Product with Serializable

   

   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.

4. case class AddReducableModelElement(facts: Conjunction, constants: Set[ConstantTerm], reducerSettings: ReducerSettings) extends Action with Product with Serializable

   

   Record that values of the given constants can be reconstructed from the provided facts.

5. case class AxiomSplit(assumptions: Seq[Formula], cases: Seq[(Conjunction, Seq[Action])], theory: Theory) extends Action with Product with Serializable

   

   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.

6. case class CloseByAxiom(assumptions: Seq[Formula], theory: Theory) extends Action with Product with Serializable

   

   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.

7. case class CutSplit(cutFormula: Conjunction, leftCase: Seq[Action], rightCase: Seq[Action]) extends Action with Product with Serializable

   

   Split a proof goal by applying the cut rule.

8. case class RemoveFacts(facts: Conjunction) extends Action with Product with Serializable

   

   Remove some facts from the handled proof goal.

9. case class ScheduleTask(proc: TheoryProcedure, priority: Int) extends Action with Product with Serializable

   

   Schedule a task to be applied later on the goal.

10. case class SplitDisequality(equality: LinearCombination, leftActions: Seq[Action], rightActions: Seq[Action]) extends Action with Product with Serializable

    

    Split a disequality fact into two inequalities.

11. case class SplitGoal(cases: Seq[Seq[Action]]) extends Action with Product with Serializable

    

    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.