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. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. def +(other: String): String
    Implicit
    This member is added by an implicit conversion from LocalProver toany2stringadd[LocalProver] performed by method any2stringadd in scala.Predef.
    Definition Classes
    any2stringadd
  4. def ->[B](y: B): (LocalProver, B)
    Implicit
    This member is added by an implicit conversion from LocalProver toArrowAssoc[LocalProver] performed by method ArrowAssoc in scala.Predef.
    Definition Classes
    ArrowAssoc
    Annotations
    @inline()
  5. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  6. def addAxioms(typs: (Typ[Term], Double)*): LocalProver
  7. def addGoal(goal: Typ[Term], weight: Double): LocalProverStep
    Definition Classes
    LocalProverStep
  8. def addGoals(typs: (Typ[Term], Double)*): LocalProver
  9. def addInd(typ: Typ[Term], intros: Term*)(params: Vector[Term] = Vector(), weight: Double = 1): LocalProver
  10. def addIndexedInd(typ: Term, intros: Term*)(params: Vector[Term] = Vector(), weight: Double = 1): LocalProver
  11. def addLookup(ts: Set[Term]): LocalProverStep
    Definition Classes
    LocalProverStep
  12. def addSolver(s: TypSolver): LocalProverStep
    Definition Classes
    LocalProverStep
  13. def addTerms(terms: (Term, Double)*): LocalProver
  14. def addTypes(typs: (Typ[Term], Double)*): LocalProver
  15. def addVar(term: Term, weight: Double): LocalProver
    Definition Classes
    LocalProver → LocalProverStep
  16. def addVars(terms: (Term, Double)*): LocalProver
  17. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  18. def backwardWeight(w: Double): LocalProver
  19. def bigExpressionEval(additional: Set[Equation]): Task[ExpressionEquationSolver]
    Definition Classes
    LocalProverStep
  20. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
  21. val cutoff: Double
    Definition Classes
    LocalProver → LocalProverStep
  22. val decay: Double
    Definition Classes
    LocalProver → LocalProverStep
  23. def distTangentProver(fd: FiniteDistribution[Term], tangentCutoff: Double = cutoff): Task[LocalTangentProver]
    Definition Classes
    LocalProverStep
  24. lazy val enhancedEquationNodes: Task[Set[EquationNode]]
    Definition Classes
    LocalProverStep
  25. lazy val enhancedExpressionEval: Task[ExpressionEquationSolver]
    Definition Classes
    LocalProverStep
  26. def ensuring(cond: (LocalProver) => Boolean, msg: => Any): LocalProver
    Implicit
    This member is added by an implicit conversion from LocalProver toEnsuring[LocalProver] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  27. def ensuring(cond: (LocalProver) => Boolean): LocalProver
    Implicit
    This member is added by an implicit conversion from LocalProver toEnsuring[LocalProver] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  28. def ensuring(cond: Boolean, msg: => Any): LocalProver
    Implicit
    This member is added by an implicit conversion from LocalProver toEnsuring[LocalProver] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  29. def ensuring(cond: Boolean): LocalProver
    Implicit
    This member is added by an implicit conversion from LocalProver toEnsuring[LocalProver] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  30. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  31. lazy val equationNodes: Task[Set[EquationNode]]
    Definition Classes
    LocalProver → LocalProverStep
  32. lazy val equations: Task[Set[Equation]]
    Definition Classes
    LocalProverStep
  33. lazy val evolvedState: Task[EvolvedState]
    Definition Classes
    LocalProverStep
  34. val exponent: Double
    Definition Classes
    LocalProver → LocalProverStep
  35. lazy val expressionEval: Task[ExpressionEquationSolver]
    Definition Classes
    LocalProverStep
  36. def formatted(fmtstr: String): String
    Implicit
    This member is added by an implicit conversion from LocalProver toStringFormat[LocalProver] performed by method StringFormat in scala.Predef.
    Definition Classes
    StringFormat
    Annotations
    @inline()
  37. lazy val functionsForGoals: Task[FiniteDistribution[Term]]
    Definition Classes
    LocalProverStep
  38. val genMaxDepth: Option[Int]
    Definition Classes
    LocalProver → LocalProverStep
  39. lazy val generatorIterant: Iterant[Task, FiniteDistribution[Term]]
    Definition Classes
    LocalProverStep
  40. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  41. val hW: Double
    Definition Classes
    LocalProver → LocalProverStep
  42. def halt(): Unit
    Definition Classes
    LocalProverStep
  43. def halted(): Boolean
    Definition Classes
    LocalProverStep
  44. val initState: TermState
    Definition Classes
    LocalProver → LocalProverStep
  45. val isHalted: Boolean
    Definition Classes
    LocalProverStep
  46. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  47. def isleWeight(w: Double): LocalProver
  48. val klW: Double
    Definition Classes
    LocalProver → LocalProverStep
  49. lazy val lemmaProofs: Task[FiniteDistribution[Term]]
    Definition Classes
    LocalProverStep
  50. lazy val lemmas: Task[Vector[(Typ[Term], Double)]]
    Definition Classes
    LocalProverStep
  51. val limit: FiniteDuration
    Definition Classes
    LocalProver → LocalProverStep
  52. val maxDepth: Int
    Definition Classes
    LocalProver → LocalProverStep
  53. val maxRatio: Double
    Definition Classes
    LocalProver → LocalProverStep
  54. val maxTime: Option[Long]
    Definition Classes
    LocalProver → LocalProverStep
  55. lazy val mf: MonixFiniteDistribution[TermState]
  56. lazy val mfd: MonixFiniteDistributionEq[TermState]
  57. def natInduction(w: Double = 1.0): LocalProver
  58. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  59. def negateTypes(w: Double): LocalProver
  60. lazy val nextState: Task[TermState]
    Definition Classes
    LocalProver → LocalProverStep
  61. lazy val nextStateDirect: Task[TermState]
  62. lazy val noIsles: LocalProver
  63. def nodeDist[Y](node: GeneratorNode[Y]): Task[FiniteDistribution[Y]]
  64. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  65. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  66. lazy val optimalInit: Task[LocalProver]
  67. lazy val optimalInit0: Task[LocalProver]
  68. lazy val orderedUnknowns: Task[Vector[Typ[Term]]]
    Definition Classes
    LocalProverStep
  69. def params(params: TermGenParams): LocalProver
  70. def productElementNames: Iterator[String]
    Definition Classes
    Product
  71. lazy val proofComponents: Task[Vector[(Term, Double)]]
    Definition Classes
    LocalProverStep
  72. def proofTangent(tangentCutoff: Double = cutoff): Task[LocalTangentProver]
    Definition Classes
    LocalProverStep
  73. lazy val proofTerms: Task[Vector[(Term, Double)]]
    Definition Classes
    LocalProverStep
  74. val relativeEval: Boolean
    Definition Classes
    LocalProver → LocalProverStep
  75. def reset(): Unit
    Definition Classes
    LocalProverStep
  76. val resolution: Double
    Definition Classes
    LocalProver → LocalProverStep
  77. val scale: Double
    Definition Classes
    LocalProver → LocalProverStep
  78. def scaleLimit(scale: Double): LocalProverStep
    Definition Classes
    LocalProverStep
  79. def scaledSplitLemmaProvers(scale: Double = 1.0): Task[Vector[LocalTangentProver]]
    Definition Classes
    LocalProverStep
  80. lazy val seek: Task[FiniteDistribution[Term]]
    Definition Classes
    LocalProverStep
  81. def sharpen(scale: Double = 2.0): LocalProver
    Definition Classes
    LocalProver → LocalProverStep
  82. val smoothing: Option[Double]
    Definition Classes
    LocalProver → LocalProverStep
  83. def splitLemmaProvers(scale: Double = 1): Task[Vector[LocalTangentProver]]
    Definition Classes
    LocalProverStep
  84. def splitTangentProvers(terms: Vector[(Term, Double)]): Task[Vector[LocalTangentProver]]
    Definition Classes
    LocalProverStep
  85. val stateFromEquation: Boolean
    Definition Classes
    LocalProver → LocalProverStep
  86. val steps: Int
    Definition Classes
    LocalProver → LocalProverStep
  87. lazy val subGoals: Task[FiniteDistribution[Typ[Term]]]
    Definition Classes
    LocalProverStep
  88. lazy val successes: Task[Vector[(Typ[Term], Double, Term)]]
    Definition Classes
    LocalProverStep
  89. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  90. def tangentExpressionEval(x: Term, weight: Double = 1.0): Task[ExpressionEquationSolver]
    Definition Classes
    LocalProverStep
  91. def tangentProver(xs: Term*): Task[LocalTangentProver]
    Definition Classes
    LocalProverStep
  92. val tg: TermGenParams
    Definition Classes
    LocalProver → LocalProverStep
  93. lazy val theoremsByProof: Task[FiniteDistribution[Typ[Term]]]
    Definition Classes
    LocalProverStep
  94. lazy val theoremsByStatement: Task[FiniteDistribution[Typ[Term]]]
    Definition Classes
    LocalProverStep
  95. lazy val tripleT: Task[(FiniteDistribution[Term], Set[EquationNode], EqDistMemo[TermState])]
  96. lazy val tripleTypT: Task[(FiniteDistribution[Typ[Term]], Set[EquationNode], EqDistMemo[TermState])]
  97. lazy val tunedGenerators: Task[FiniteDistribution[Term]]
    Definition Classes
    LocalProverStep
  98. lazy val tunedInit: Task[LocalProver]
  99. lazy val typesByMap: LocalProver
  100. lazy val typesByRestrict: LocalProver
  101. lazy val unknownStatements: Task[FiniteDistribution[Typ[Term]]]
    Definition Classes
    LocalProverStep
  102. def varDist[Y](rv: RandomVar[Y]): Task[FiniteDistribution[Y]]
  103. def varDistEqs[Y](rv: RandomVar[Y]): Task[(FiniteDistribution[Y], Set[EquationNode])]
  104. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  105. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  106. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  107. def withCutoff(ctf: Double): LocalProver
    Definition Classes
    LocalProver → LocalProverStep
  108. def withInit(ts: TermState): LocalProver
    Definition Classes
    LocalProver → LocalProverStep
  109. lazy val withLemmas: Task[LocalProver]
  110. def withLimit(l: FiniteDuration): LocalProver
    Definition Classes
    LocalProver → LocalProverStep
  111. def withParams(p: TermGenParams): LocalProver
    Definition Classes
    LocalProver → LocalProverStep

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated
  2. def →[B](y: B): (LocalProver, B)
    Implicit
    This member is added by an implicit conversion from LocalProver toArrowAssoc[LocalProver] performed by method ArrowAssoc in scala.Predef.
    Definition Classes
    ArrowAssoc
    Annotations
    @deprecated
    Deprecated

    (Since version 2.13.0) Use -> instead. If you still wish to display it as one character, consider using a font with programming ligatures such as Fira Code.

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from LocalProverStep

Inherited from AnyRef

Inherited from Any

Inherited by implicit conversion any2stringadd fromLocalProver to any2stringadd[LocalProver]

Inherited by implicit conversion StringFormat fromLocalProver to StringFormat[LocalProver]

Inherited by implicit conversion Ensuring fromLocalProver to Ensuring[LocalProver]

Inherited by implicit conversion ArrowAssoc fromLocalProver to ArrowAssoc[LocalProver]

Ungrouped