Package

ap.proof

tree

Permalink

package tree

Visibility
  1. Public
  2. All

Type Members

  1. class AndTree extends ProofTree

    Permalink
  2. class IteratingProofTreeFactory extends SimpleProofTreeFactory

    Permalink

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

  3. trait ProofTree extends AnyRef

    Permalink
  4. abstract class ProofTreeFactory extends AnyRef

    Permalink
  5. trait ProofTreeOneChild extends ProofTree

    Permalink

    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

    Permalink

    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

  7. abstract class RandomDataSource extends AnyRef

    Permalink

    Class to produce data needed to randomise proof construction.

  8. class SeededRandomDataSource extends RandomDataSource

    Permalink

    Source producing random data.

  9. class SimpleProofTreeFactory extends ProofTreeFactory

    Permalink
  10. class StrengthenTree extends ProofTreeOneChild

    Permalink

    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

  11. class WeakenTree extends ProofTreeOneChild

    Permalink

    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

Value Members

  1. object AndTree

    Permalink
  2. object NonRandomDataSource extends RandomDataSource

    Permalink

    Source producing non-random data.

  3. object ProofTree

    Permalink
  4. object ProofTreeOneChild

    Permalink
  5. object QuantifiedTree

    Permalink
  6. object StrengthenTree

    Permalink
  7. object TestProofTree

    Permalink
  8. object WeakenTree

    Permalink

Ungrouped