Packages

o

provingground.learning

FineProverTasks

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.

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. FineProverTasks
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Value Members

  1. 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.

  2. 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

  3. 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.

  4. 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.

  5. 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

  6. 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.

  7. 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.

  8. 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.

  9. 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.

  10. 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

  11. 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.

  12. 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.