Packages

t

provingground.learning

LocalProverStep

trait LocalProverStep extends AnyRef

Linear Supertypes
AnyRef, Any
Known Subclasses
LocalProver, LocalTangentProver
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. LocalProverStep
  2. AnyRef
  3. Any
Implicitly
  1. by any2stringadd
  2. by StringFormat
  3. by Ensuring
  4. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Abstract Value Members

  1. abstract val cutoff: Double
  2. abstract val decay: Double
  3. abstract val equationNodes: Task[Set[EquationNode]]
  4. abstract val exponent: Double
  5. abstract val genMaxDepth: Option[Int]
  6. abstract val hW: Double
  7. abstract val initState: TermState
  8. abstract val klW: Double
  9. abstract val limit: FiniteDuration
  10. abstract val maxDepth: Int
  11. abstract val maxRatio: Double
  12. abstract val maxTime: Option[Long]
  13. abstract val nextState: Task[TermState]
  14. abstract val relativeEval: Boolean
  15. abstract val resolution: Double
  16. abstract val scale: Double
  17. abstract val smoothing: Option[Double]
  18. abstract val stateFromEquation: Boolean
  19. abstract val steps: Int
  20. abstract val tg: TermGenParams
  21. abstract def withCutoff(cutoff: Double): LocalProverStep
  22. abstract def withInit(ts: TermState): LocalProverStep
  23. abstract def withLimit(l: FiniteDuration): LocalProverStep
  24. abstract def withParams(p: TermGenParams): LocalProverStep

Concrete Value Members

  1. def addGoal(goal: Typ[Term], weight: Double): LocalProverStep
  2. def addLookup(ts: Set[Term]): LocalProverStep
  3. def addSolver(s: TypSolver): LocalProverStep
  4. def addVar(term: Term, weight: Double): LocalProverStep
  5. def bigExpressionEval(additional: Set[Equation]): Task[ExpressionEquationSolver]
  6. def distTangentProver(fd: FiniteDistribution[Term], tangentCutoff: Double = cutoff): Task[LocalTangentProver]
  7. lazy val enhancedEquationNodes: Task[Set[EquationNode]]
  8. lazy val enhancedExpressionEval: Task[ExpressionEquationSolver]
  9. lazy val equations: Task[Set[Equation]]
  10. lazy val evolvedState: Task[EvolvedState]
  11. lazy val expressionEval: Task[ExpressionEquationSolver]
  12. lazy val functionsForGoals: Task[FiniteDistribution[Term]]
  13. lazy val generatorIterant: Iterant[Task, FiniteDistribution[Term]]
  14. def halt(): Unit
  15. def halted(): Boolean
  16. val isHalted: Boolean
  17. lazy val lemmaProofs: Task[FiniteDistribution[Term]]
  18. lazy val lemmas: Task[Vector[(Typ[Term], Double)]]
  19. lazy val orderedUnknowns: Task[Vector[Typ[Term]]]
  20. lazy val proofComponents: Task[Vector[(Term, Double)]]
  21. def proofTangent(tangentCutoff: Double = cutoff): Task[LocalTangentProver]
  22. lazy val proofTerms: Task[Vector[(Term, Double)]]
  23. def reset(): Unit
  24. def scaleLimit(scale: Double): LocalProverStep
  25. def scaledSplitLemmaProvers(scale: Double = 1.0): Task[Vector[LocalTangentProver]]
  26. lazy val seek: Task[FiniteDistribution[Term]]
  27. def sharpen(scale: Double = 2.0): LocalProverStep
  28. def splitLemmaProvers(scale: Double = 1): Task[Vector[LocalTangentProver]]
  29. def splitTangentProvers(terms: Vector[(Term, Double)]): Task[Vector[LocalTangentProver]]
  30. lazy val subGoals: Task[FiniteDistribution[Typ[Term]]]
  31. lazy val successes: Task[Vector[(Typ[Term], Double, Term)]]
  32. def tangentExpressionEval(x: Term, weight: Double = 1.0): Task[ExpressionEquationSolver]
  33. def tangentProver(xs: Term*): Task[LocalTangentProver]
  34. lazy val theoremsByProof: Task[FiniteDistribution[Typ[Term]]]
  35. lazy val theoremsByStatement: Task[FiniteDistribution[Typ[Term]]]
  36. lazy val tunedGenerators: Task[FiniteDistribution[Term]]
  37. lazy val unknownStatements: Task[FiniteDistribution[Typ[Term]]]