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 subtree
ProofTreeOneChild
that quantifies a set of constants in
the closing constraint of its subtree
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 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
ProofTreeOneChild
that weakens the closing constraint of its
subtree
by disjunctively adding a formula
Source producing non-random data.
Common superclass for proof trees that have exactly one direct subtree. Such trees know about two
TermOrder
s: theTermOrder
of the closing constraint coming from the subtree, and theTermOrder
of the constraint of thisProofTree