object FineProverTasks
A collection of functions to build provers;
some are abstract methods for exploring, searching etc., while others generate terms and types, sometimes as derivatives.
Some methods combine the two to give a ready to use function.
These are based on TermEvolver and Monix.
- Alphabetic
- By Inheritance
- FineProverTasks
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
- def dervecMemoTasks(base: FiniteDistribution[Term], tv: TermEvolver, termsTask: Task[FiniteDistribution[Term]], typsTask: Task[FiniteDistribution[Typ[Term]]], maxtime: FiniteDuration, cutoff: Double, scale: Double, trace: Vector[Term], termSet: Set[Term], typSet: Set[Typ[Term]], vars: Vector[Term] = Vector()): Task[Vector[Task[(FiniteDistribution[Term], Vector[Term], Set[Term], Set[Typ[Term]])]]]
bunch of tasks using newly discovered proofs by evolving along unit tangents.
bunch of tasks using newly discovered proofs by evolving along unit tangents. the cutoffs, viewed as resources, are allocated based on values of the new proofs. these tasks return the tangent distributions as well as the path to get there.
- def dervecTasks(base: FiniteDistribution[Term], tv: TermEvolver, termsTask: Task[FiniteDistribution[Term]], typsTask: Task[FiniteDistribution[Typ[Term]]], maxtime: FiniteDuration, cutoff: Double, scale: Double, vars: Vector[Term] = Vector()): Task[Vector[Task[FiniteDistribution[Term]]]]
bunch of tasks using newly discovered proofs by evolving along unit tangents.
bunch of tasks using newly discovered proofs by evolving along unit tangents. the cutoffs, viewed as resources, are allocated based on values of the new proofs. these tasks only return the tangent distributions
- def dervecTraceTasks(base: FiniteDistribution[Term], tv: TermEvolver, termsTask: Task[FiniteDistribution[Term]], typsTask: Task[FiniteDistribution[Typ[Term]]], maxtime: FiniteDuration, cutoff: Double, scale: Double, trace: Vector[Term], vars: Vector[Term] = Vector()): Task[Vector[Task[(FiniteDistribution[Term], Vector[Term])]]]
bunch of tasks using newly discovered proofs by evolving along unit tangents.
bunch of tasks using newly discovered proofs by evolving along unit tangents. the cutoffs, viewed as resources, are allocated based on values of the new proofs. these tasks return the tangent distributions as well as the path to get there.
- def dervecWeightedTraceTasks(base: FiniteDistribution[Term], tv: TermEvolver, termsTask: Task[FiniteDistribution[Term]], typsTask: Task[FiniteDistribution[Typ[Term]]], maxtime: FiniteDuration, cutoff: Double, scale: Double, trace: Vector[(Term, Double)], vars: Vector[Term] = Vector()): Task[Vector[Task[(FiniteDistribution[Term], Vector[(Term, Double)])]]]
bunch of tasks using newly discovered proofs by evolving along unit tangents.
bunch of tasks using newly discovered proofs by evolving along unit tangents. the cutoffs, viewed as resources, are allocated based on values of the new proofs. these tasks return the tangent distributions as well as the path to get there, plus weights of proofs as they are found.
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def termdistDerTask(fd: FiniteDistribution[Term], tfd: FiniteDistribution[Term], tv: TermEvolver, cutoff: Double, maxtime: FiniteDuration, vars: Vector[Term] = Vector()): Task[FiniteDistribution[Term]]
evolution of terms by the derivative, as a (task with value) finite distribution; obtained by lazy recursive definition in TermEvolver and trunctation.
evolution of terms by the derivative, as a (task with value) finite distribution; obtained by lazy recursive definition in TermEvolver and trunctation.
- fd
the distribution point
- tfd
the tangent distribution
- tv
the term evolver
- def termdistTask(fd: FiniteDistribution[Term], tv: TermEvolver, cutoff: Double, maxtime: FiniteDuration, vars: Vector[Term] = Vector()): Task[FiniteDistribution[Term]]
evolution of terms, as a (task with value) finite distribution; obtained by lazy recursive definition in TermEvolver and trunctation.
- def theoremSearchMemoTask(fd: FiniteDistribution[Term], tv: TermEvolver, cutoff: Double, maxtime: FiniteDuration, goal: Typ[Term], termSet: Set[Term], typSet: Set[Typ[Term]], decay: Double = 1.0, scale: Double = 1.0, vars: Vector[Term] = Vector()): Task[Option[(Term, Vector[Term], Set[Term], Set[Typ[Term]])]]
breadth-first search for a term of a given type, keeping track of the path and the distributions along the way
breadth-first search for a term of a given type, keeping track of the path and the distributions along the way
- returns
task giving an optional term of the type together with a vector of proofs of lemmas.
- def theoremSearchTask(fd: FiniteDistribution[Term], tv: TermEvolver, cutoff: Double, maxtime: FiniteDuration, goal: Typ[Term], decay: Double = 1.0, scale: Double = 1.0, vars: Vector[Term] = Vector()): Task[Option[Term]]
breadth-first search for a term of a given type
breadth-first search for a term of a given type
- returns
task giving an optional term of the type.
- def theoremSearchTraceTask(fd: FiniteDistribution[Term], tv: TermEvolver, cutoff: Double, maxtime: FiniteDuration, goal: Typ[Term], decay: Double = 1.0, scale: Double = 1.0, vars: Vector[Term] = Vector()): Task[Option[(Term, Vector[Term])]]
breadth-first search for a term of a given type, keeping track of the path
breadth-first search for a term of a given type, keeping track of the path
- returns
task giving an optional term of the type together with a vector of proofs of lemmas.
- def theoremsExploreTask(fd: FiniteDistribution[Term], tv: TermEvolver, cutoff: Double, maxtime: FiniteDuration, decay: Double = 1.0, scale: Double = 1.0, vars: Vector[Term] = Vector()): Task[Map[Typ[Term], Vector[(Term, (Int, Double))]]]
breadth-first exploration to find alll interesting proofs.
breadth-first exploration to find alll interesting proofs.
- returns
map from types to proofs with weights and steps
- def theoremsExploreTraceTask(fd: FiniteDistribution[Term], tv: TermEvolver, cutoff: Double, maxtime: FiniteDuration, decay: Double = 1.0, scale: Double = 1.0, vars: Vector[Term] = Vector()): Task[(Vector[(Term, Vector[(Term, Double)], (Int, Double))], FiniteDistribution[Term], FiniteDistribution[Typ[Term]])]
breadth-first exploration to find alll interesting proofs, keeping track of lemmas
breadth-first exploration to find alll interesting proofs, keeping track of lemmas
- returns
task for vector of proofs with lemmas and the corresponding theorems.
- def toString(): String
- Definition Classes
- AnyRef → Any
- def typdistTask(fd: FiniteDistribution[Term], tv: TermEvolver, cutoff: Double, maxtime: FiniteDuration, vars: Vector[Term] = Vector()): Task[FiniteDistribution[Typ[Term]]]
evolution of types, as a (task with value) finite distribution; obtained by lazy recursive definition in TermEvolver and trunctation.
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated