Type Members

1.  class AndTree extends ProofTree
2.  class IteratingProofTreeFactory extends SimpleProofTreeFactory

   Proof tree factory in which updating a goal will recursive apply further rules, until some stopping condition holds

3.  trait ProofTree extends AnyRef
4.  abstract class ProofTreeFactory extends AnyRef
5.  trait ProofTreeOneChild extends ProofTree

   Common superclass for proof trees that have exactly one direct subtree.

   Common superclass for proof trees that have exactly one direct subtree. Such trees know about two TermOrders: the TermOrder of the closing constraint coming from the subtree, and the TermOrder of the constraint of this ProofTree

6.  class QuantifiedTree extends ProofTreeOneChild

   ProofTreeOneChild that quantifies a set of constants in the closing constraint of its subtree

7.  abstract class RandomDataSource extends AnyRef

   Class to produce data needed to randomise proof construction.

8.  class SeededRandomDataSource extends RandomDataSource

   Source producing random data.

9.  class SimpleProofTreeFactory extends ProofTreeFactory
10.  class StrengthenTree extends ProofTreeOneChild

    ProofTreeOneChild that strengthens the closing constraint of its subtree by conjoining a formula

11.  class WeakenTree extends ProofTreeOneChild

    ProofTreeOneChild that weakens the closing constraint of its subtree by disjunctively adding a formula