Type Members

1.  case class DeltaTableMethod(singleQuantifier: Boolean = false, subsumedRowMerging: Boolean = false, keyLimit: Option[Int] = None) extends GrammarFindingMethod with Product with Serializable
2.  abstract class GeneralLeastGeneralGeneralization extends AnyRef
3.  case class InductionGrammar(tau: Var, alpha: Var, nus: Map[Const, NonTerminalVect], gamma: List[Var], productions: Vector[Production]) extends Product with Serializable
4.  case class InductionGrammarMinimizationFormula(g: InductionGrammar) extends Product with Serializable
5.  class Pi2Grammar extends Pi2PreGrammar
6.  case class Pi2PreGrammar(startSymbol: Var, alpha: Var, betas: Vector[Var], productions: Vector[(Var, Expr)]) extends Product with Serializable

   This is a slightly batshit insane and completely wrong formalization of grammars for proofs with a single Π₂-cut.

   This is a slightly batshit insane and completely wrong formalization of grammars for proofs with a single Π₂-cut. (Should be isomorphic to the usual versions though.)

   Say ∀x ∃y φ(x,y) is the cut-formula.

   Then the left side of the cut has one strong quantifier inference (with eigenvariable α), and many weak quantifier inferences (with terms t). Each weak quantifier inference is stored as the production α → t (yes, yes, and also, t may contain α).

   The right side of the cut has alternating weak and strong quantifier inferences. Say r is the term of the weak quantifier inference, then β is the eigenvariable such that φ(r,β). We store this as the production β → r. Additionally, we require that there is *exactly one* production for each β (this condition is missing from pre-grammars)

7.  class RecSchemGenLangFormula extends AnyRef
8.  case class RecSchemTemplate(startSymbol: Const, template: Set[(Expr, Expr)]) extends Product with Serializable
9.  case class RecursionScheme(startSymbol: Const, nonTerminals: Set[Const], rules: Set[Rule]) extends Product with Serializable
10.  case class Rule(lhs: Expr, rhs: Expr) extends Product with Serializable
11.  case class VTRATG(startSymbol: Var, nonTerminals: Seq[NonTerminalVect], productions: Set[Production]) extends Product with Serializable
12.  class VectGrammarMinimizationFormula extends AnyRef
13.  case class VtratgParameter(nonTerminalTypes: Seq[Seq[TBase]]) extends Product with Serializable
14.  class VtratgTermGenerationFormula extends AnyRef
15.  class leastGeneralGeneralization extends AnyRef