object MonixProverTasks
A drop-in replacement for FineProverTasks to test the abstract generators approach; since testing is the goal redundancies and some comments have been removed.
- Alphabetic
- By Inheritance
- MonixProverTasks
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Value Members
- def dervecTraceTasks(base: FiniteDistribution[Term], tg: TermGenParams, 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], tg: TermGenParams, 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.
- def termdistDerTask(fd: FiniteDistribution[Term], tfd: FiniteDistribution[Term], tg: TermGenParams, cutoff: Double, maxtime: FiniteDuration, vars: Vector[Term] = Vector()): Task[FiniteDistribution[Term]]
- def termdistTask(fd: FiniteDistribution[Term], tg: TermGenParams, cutoff: Double, maxtime: FiniteDuration, vars: Vector[Term] = Vector()): Task[FiniteDistribution[Term]]
- def theoremSearchTraceTask(fd: FiniteDistribution[Term], tg: TermGenParams, 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 theoremsExploreTraceTask(fd: FiniteDistribution[Term], tg: TermGenParams, 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 typdistTask(fd: FiniteDistribution[Term], tg: TermGenParams, cutoff: Double, maxtime: FiniteDuration, vars: Vector[Term] = Vector()): Task[FiniteDistribution[Typ[Term]]]
- def typs(fd: FiniteDistribution[Term]): FiniteDistribution[Typ[Term]]