Proof tree factory in which updating a goal will recursive apply further rules, until some stopping condition holds
Common superclass for proof trees that have exactly one direct subtree.
ProofTreeOneChild that quantifies a set of constants in
the closing constraint of its
Class to produce data needed to randomise proof construction.
Source producing random data.
ProofTreeOneChild that strengthens the closing constraint of its
subtree by conjoining a formula
ProofTreeOneChild that weakens the closing constraint of its
subtree by disjunctively adding a formula