Packages

case class LocalProver(initState: TermState = TermState(FiniteDistribution.empty, FiniteDistribution.empty), tg: TermGenParams = TermGenParams(), cutoff: Double = math.pow(10, -4), genMaxDepth: Option[Int] = None, limit: FiniteDuration = 12.minutes, maxRatio: Double = 1.01, resolution: Double = 0.0, scale: Double = 1.0, steps: Int = 10000, maxDepth: Int = 10, hW: Double = 1, klW: Double = 1, smoothing: Option[Double] = None, relativeEval: Boolean = false, stateFromEquation: Boolean = false, exponent: Double = 0.5, decay: Double = 1, maxTime: Option[Long] = None) extends LocalProverStep with Product with Serializable

Collect local/generative/tactical proving; this includes configuration and learning but excludes strategy and attention. This can be called in a loop generating goals based on unproved theorems, using representation/deep learning with attention focussed or interactively.

Linear Supertypes
Serializable, Product, Equals, LocalProverStep, AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. LocalProver
  2. Serializable
  3. Product
  4. Equals
  5. LocalProverStep
  6. AnyRef
  7. 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

Instance Constructors

  1. new LocalProver(initState: TermState = TermState(FiniteDistribution.empty, FiniteDistribution.empty), tg: TermGenParams = TermGenParams(), cutoff: Double = math.pow(10, -4), genMaxDepth: Option[Int] = None, limit: FiniteDuration = 12.minutes, maxRatio: Double = 1.01, resolution: Double = 0.0, scale: Double = 1.0, steps: Int = 10000, maxDepth: Int = 10, hW: Double = 1, klW: Double = 1, smoothing: Option[Double] = None, relativeEval: Boolean = false, stateFromEquation: Boolean = false, exponent: Double = 0.5, decay: Double = 1, maxTime: Option[Long] = None)

Value Members

  1. def addAxioms(typs: (Typ[Term], Double)*): LocalProver
  2. def addGoal(goal: Typ[Term], weight: Double): LocalProverStep
    Definition Classes
    LocalProverStep
  3. def addGoals(typs: (Typ[Term], Double)*): LocalProver
  4. def addInd(typ: Typ[Term], intros: Term*)(params: Vector[Term] = Vector(), weight: Double = 1): LocalProver
  5. def addIndexedInd(typ: Term, intros: Term*)(params: Vector[Term] = Vector(), weight: Double = 1): LocalProver
  6. def addLookup(ts: Set[Term]): LocalProverStep
    Definition Classes
    LocalProverStep
  7. def addSolver(s: TypSolver): LocalProverStep
    Definition Classes
    LocalProverStep
  8. def addTerms(terms: (Term, Double)*): LocalProver
  9. def addTypes(typs: (Typ[Term], Double)*): LocalProver
  10. def addVar(term: Term, weight: Double): LocalProver
    Definition Classes
    LocalProver → LocalProverStep
  11. def addVars(terms: (Term, Double)*): LocalProver
  12. def backwardWeight(w: Double): LocalProver
  13. def bigExpressionEval(additional: Set[Equation]): Task[ExpressionEquationSolver]
    Definition Classes
    LocalProverStep
  14. val cutoff: Double
    Definition Classes
    LocalProver → LocalProverStep
  15. val decay: Double
    Definition Classes
    LocalProver → LocalProverStep
  16. def distTangentProver(fd: FiniteDistribution[Term], tangentCutoff: Double = cutoff): Task[LocalTangentProver]
    Definition Classes
    LocalProverStep
  17. lazy val enhancedEquationNodes: Task[Set[EquationNode]]
    Definition Classes
    LocalProverStep
  18. lazy val enhancedExpressionEval: Task[ExpressionEquationSolver]
    Definition Classes
    LocalProverStep
  19. lazy val equationNodes: Task[Set[EquationNode]]
    Definition Classes
    LocalProver → LocalProverStep
  20. lazy val equations: Task[Set[Equation]]
    Definition Classes
    LocalProverStep
  21. lazy val evolvedState: Task[EvolvedState]
    Definition Classes
    LocalProverStep
  22. val exponent: Double
    Definition Classes
    LocalProver → LocalProverStep
  23. lazy val expressionEval: Task[ExpressionEquationSolver]
    Definition Classes
    LocalProverStep
  24. lazy val functionsForGoals: Task[FiniteDistribution[Term]]
    Definition Classes
    LocalProverStep
  25. val genMaxDepth: Option[Int]
    Definition Classes
    LocalProver → LocalProverStep
  26. lazy val generatorIterant: Iterant[Task, FiniteDistribution[Term]]
    Definition Classes
    LocalProverStep
  27. val hW: Double
    Definition Classes
    LocalProver → LocalProverStep
  28. def halt(): Unit
    Definition Classes
    LocalProverStep
  29. def halted(): Boolean
    Definition Classes
    LocalProverStep
  30. val initState: TermState
    Definition Classes
    LocalProver → LocalProverStep
  31. val isHalted: Boolean
    Definition Classes
    LocalProverStep
  32. def isleWeight(w: Double): LocalProver
  33. val klW: Double
    Definition Classes
    LocalProver → LocalProverStep
  34. lazy val lemmaProofs: Task[FiniteDistribution[Term]]
    Definition Classes
    LocalProverStep
  35. lazy val lemmas: Task[Vector[(Typ[Term], Double)]]
    Definition Classes
    LocalProverStep
  36. val limit: FiniteDuration
    Definition Classes
    LocalProver → LocalProverStep
  37. val maxDepth: Int
    Definition Classes
    LocalProver → LocalProverStep
  38. val maxRatio: Double
    Definition Classes
    LocalProver → LocalProverStep
  39. val maxTime: Option[Long]
    Definition Classes
    LocalProver → LocalProverStep
  40. lazy val mf: MonixFiniteDistribution[TermState]
  41. lazy val mfd: MonixFiniteDistributionEq[TermState]
  42. def natInduction(w: Double = 1.0): LocalProver
  43. def negateTypes(w: Double): LocalProver
  44. lazy val nextState: Task[TermState]
    Definition Classes
    LocalProver → LocalProverStep
  45. lazy val nextStateDirect: Task[TermState]
  46. lazy val noIsles: LocalProver
  47. def nodeDist[Y](node: GeneratorNode[Y]): Task[FiniteDistribution[Y]]
  48. lazy val optimalInit: Task[LocalProver]
  49. lazy val optimalInit0: Task[LocalProver]
  50. lazy val orderedUnknowns: Task[Vector[Typ[Term]]]
    Definition Classes
    LocalProverStep
  51. def params(params: TermGenParams): LocalProver
  52. def productElementNames: Iterator[String]
    Definition Classes
    Product
  53. lazy val proofComponents: Task[Vector[(Term, Double)]]
    Definition Classes
    LocalProverStep
  54. def proofTangent(tangentCutoff: Double = cutoff): Task[LocalTangentProver]
    Definition Classes
    LocalProverStep
  55. lazy val proofTerms: Task[Vector[(Term, Double)]]
    Definition Classes
    LocalProverStep
  56. val relativeEval: Boolean
    Definition Classes
    LocalProver → LocalProverStep
  57. def reset(): Unit
    Definition Classes
    LocalProverStep
  58. val resolution: Double
    Definition Classes
    LocalProver → LocalProverStep
  59. val scale: Double
    Definition Classes
    LocalProver → LocalProverStep
  60. def scaleLimit(scale: Double): LocalProverStep
    Definition Classes
    LocalProverStep
  61. def scaledSplitLemmaProvers(scale: Double = 1.0): Task[Vector[LocalTangentProver]]
    Definition Classes
    LocalProverStep
  62. lazy val seek: Task[FiniteDistribution[Term]]
    Definition Classes
    LocalProverStep
  63. def sharpen(scale: Double = 2.0): LocalProver
    Definition Classes
    LocalProver → LocalProverStep
  64. val smoothing: Option[Double]
    Definition Classes
    LocalProver → LocalProverStep
  65. def splitLemmaProvers(scale: Double = 1): Task[Vector[LocalTangentProver]]
    Definition Classes
    LocalProverStep
  66. def splitTangentProvers(terms: Vector[(Term, Double)]): Task[Vector[LocalTangentProver]]
    Definition Classes
    LocalProverStep
  67. val stateFromEquation: Boolean
    Definition Classes
    LocalProver → LocalProverStep
  68. val steps: Int
    Definition Classes
    LocalProver → LocalProverStep
  69. lazy val subGoals: Task[FiniteDistribution[Typ[Term]]]
    Definition Classes
    LocalProverStep
  70. lazy val successes: Task[Vector[(Typ[Term], Double, Term)]]
    Definition Classes
    LocalProverStep
  71. def tangentExpressionEval(x: Term, weight: Double = 1.0): Task[ExpressionEquationSolver]
    Definition Classes
    LocalProverStep
  72. def tangentProver(xs: Term*): Task[LocalTangentProver]
    Definition Classes
    LocalProverStep
  73. val tg: TermGenParams
    Definition Classes
    LocalProver → LocalProverStep
  74. lazy val theoremsByProof: Task[FiniteDistribution[Typ[Term]]]
    Definition Classes
    LocalProverStep
  75. lazy val theoremsByStatement: Task[FiniteDistribution[Typ[Term]]]
    Definition Classes
    LocalProverStep
  76. lazy val tripleT: Task[(FiniteDistribution[Term], Set[EquationNode], EqDistMemo[TermState])]
  77. lazy val tripleTypT: Task[(FiniteDistribution[Typ[Term]], Set[EquationNode], EqDistMemo[TermState])]
  78. lazy val tunedGenerators: Task[FiniteDistribution[Term]]
    Definition Classes
    LocalProverStep
  79. lazy val tunedInit: Task[LocalProver]
  80. lazy val typesByMap: LocalProver
  81. lazy val typesByRestrict: LocalProver
  82. lazy val unknownStatements: Task[FiniteDistribution[Typ[Term]]]
    Definition Classes
    LocalProverStep
  83. def varDist[Y](rv: RandomVar[Y]): Task[FiniteDistribution[Y]]
  84. def varDistEqs[Y](rv: RandomVar[Y]): Task[(FiniteDistribution[Y], Set[EquationNode])]
  85. def withCutoff(ctf: Double): LocalProver
    Definition Classes
    LocalProver → LocalProverStep
  86. def withInit(ts: TermState): LocalProver
    Definition Classes
    LocalProver → LocalProverStep
  87. lazy val withLemmas: Task[LocalProver]
  88. def withLimit(l: FiniteDuration): LocalProver
    Definition Classes
    LocalProver → LocalProverStep
  89. def withParams(p: TermGenParams): LocalProver
    Definition Classes
    LocalProver → LocalProverStep