Type Members

1.  class ClauseWithIndexLists extends AnyRef

   Combined data of many unified literals in a clause and whether the clause is a potential part of a formula in disjunctive normal form that makes all leaves of the reduced representation true

2.  class ClausesWithIndexLists extends AnyRef

   Combined data of many clauses in a set of clauses and whether the clauses translate to a formula in disjunctive normal form that makes all leaves of the reduced representation true

3.  trait GrammarFindingMethod extends AnyRef
4.  class LeafIndex extends AnyRef

   Contains two sets to store integers

5.  class LiteralWithIndexLists extends AnyRef

   Supposed to contain the data of a unified literal and whether it makes a non-tautological leaf of the reduced representation true

6.  case class MaxSATMethod(solver: MaxSATSolver, nonTerminalLengths: Int*) extends GrammarFindingMethod with Product with Serializable
7.  case class Pi2SeHs(reducedRepresentation: Sequent[Formula], universalEigenvariable: Var, existentialEigenvariables: List[Var], substitutionsForAlpha: List[Expr], substitutionsForBetaWithAlpha: List[Expr]) extends Product with Serializable

   Schematic extended Herbrand sequent for schematic Pi-2 grammars

   Schematic extended Herbrand sequent for schematic Pi-2 grammars

   reducedRepresentation

   The schematic extended Herbrand sequent without placeholder for the cut ( F[x\U_1] |- G[y\U_2] )

   universalEigenvariable

   The variable that is introduced for the universally quantified variable of the cut formula (alpha)

   existentialEigenvariables

   The variables that are introduced for the existentially quantified variable of the cut formula (beta_1,...,beta_m)

   substitutionsForAlpha

   The terms (except from the eigenvariable) that are introduced for the universally quantified variable of the cut formula (r_1,...,r_m)

   substitutionsForBetaWithAlpha

   The terms (except from the eigenvariables) that are introduced for the existentially quantified variable of the cut formula independent from the existential eigenvariables (t_1(alpha),...,t_p(alpha))

8.  case class SchematicExtendedHerbrandSequent(us: Sequent[(FOLFormula, Seq[Seq[FOLTerm]])], ss: Seq[(Seq[FOLVar], Seq[Seq[FOLTerm]])]) extends Product with Serializable

   Represents a schematic extended Herbrand sequent.

   Represents a schematic extended Herbrand sequent.

   us

   Formulas of the original end-sequent, together with their instances.

   ss

   Instances of the cut-implications.

9.  case class SolutionStructure(sehs: SchematicExtendedHerbrandSequent, formulas: Seq[FOLFormula]) extends Product with Serializable