gapt
2.19.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.cutintro/Pi2SeHs

Pi2SeHs

gapt.cutintro.Pi2SeHs
case class Pi2SeHs(reducedRepresentation: Sequent[Formula], universalEigenvariable: Var, existentialEigenvariables: List[Var], substitutionsForAlpha: List[Expr], substitutionsForBetaWithAlpha: List[Expr])

Schematic extended Herbrand sequent for schematic Pi-2 grammars

Value parameters

existentialEigenvariables

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

reducedRepresentation

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

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

universalEigenvariable

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

Attributes

Source
introducePiCut.scala
Graph
Supertypes
trait Serializable
trait Product
trait Equals
class Object
trait Matchable
class Any
Show all

Members list

Value members

Concrete methods

def herbrandSequent(): Sequent[Formula]

Computes the Herbrand sequent that corresponds to the schematic Pi-2 grammar (F[x\T_1] |- G[y\T_2])

Computes the Herbrand sequent that corresponds to the schematic Pi-2 grammar (F[x\T_1] |- G[y\T_2])

Attributes

Source
introducePiCut.scala
def sortAndAtomize(literals: Set[Formula]): (Set[Formula], Set[Formula])

Computes two sets of atoms P,N for a given set of literals such that P contains all positive literals and N all atoms of the negative literals

Computes two sets of atoms P,N for a given set of literals such that P contains all positive literals and N all atoms of the negative literals

Attributes

Source
introducePiCut.scala
def substitutionPairsBetaI(index: Int): List[(Expr, Expr)]

Pairs of a existential eigenvariable with the substitutions for this existential eigenvariable ((beta_i,t_1(alpha)),...,(beta_i,t_p(alpha)) with i=index)

Pairs of a existential eigenvariable with the substitutions for this existential eigenvariable ((beta_i,t_1(alpha)),...,(beta_i,t_p(alpha)) with i=index)

Value parameters

index

Indicates the considered existential eigenvariable (1 <= index <= m)

Attributes

Source
introducePiCut.scala
def substitutionsBetaI(index: Int): List[Substitution]

List of substitutions ((beta_i->t_1(r_i)),...,(beta_i->t_p(r_i)) with i=index)

List of substitutions ((beta_i->t_1(r_i)),...,(beta_i->t_p(r_i)) with i=index)

Value parameters

index

Indicates the considered existential eigenvariable (1 <= index <= m)

Attributes

Source
introducePiCut.scala
def theDNTAsInTheLanguage(unifiedLiterals: Set[Formula]): List[Sequent[Formula]]

List of all relevant normalized (everything is shifted to the left side) leaves of the reduced representation in a reduced signature/language that contains the unified literals (work in progress)

List of all relevant normalized (everything is shifted to the left side) leaves of the reduced representation in a reduced signature/language that contains the unified literals (work in progress)

Value parameters

unifiedLiterals

A set of formulas (unified literals) that define the reduced signature/language

Attributes

Source
introducePiCut.scala

Inherited methods

def productElementNames: Iterator[String]

Attributes

Inherited from:
Product
def productIterator: Iterator[Any]

Attributes

Inherited from:
Product

Concrete fields

val dualNonTautologicalAxioms: List[Sequent[Formula]]

The set of all relevant normalized (everything is shifted to the left side) leaves

The set of all relevant normalized (everything is shifted to the left side) leaves

Attributes

Source
introducePiCut.scala
val literalsInTheDNTAs: (Set[Formula], Set[Formula], Set[Formula])

Three sets A,B,N containing all atoms occurring in the leaves of the reduced representation (the atoms are negated if they occur on the right side of the sequent) such that in all atoms (literals) of N no eigenvariables occur, in all atoms (literals) of A only the universal eigenvariable occur, and in all atoms (literals) of B only the existential eigenvariables occur

Three sets A,B,N containing all atoms occurring in the leaves of the reduced representation (the atoms are negated if they occur on the right side of the sequent) such that in all atoms (literals) of N no eigenvariables occur, in all atoms (literals) of A only the universal eigenvariable occur, and in all atoms (literals) of B only the existential eigenvariables occur

Attributes

Source
introducePiCut.scala
val literalsInTheDNTAsAndTheDNTAs: (Set[Formula], List[Sequent[Formula]])

Computes simultaneously a set of all atoms occurring in the leaves of the reduced representation (the atoms are negated if they occur on the right side of the sequent) and a list of all relevant normalized (everything is shifted to the left side) leaves of the reduced representation

Computes simultaneously a set of all atoms occurring in the leaves of the reduced representation (the atoms are negated if they occur on the right side of the sequent) and a list of all relevant normalized (everything is shifted to the left side) leaves of the reduced representation

Attributes

Source
introducePiCut.scala
val multiplicityOfAlpha: Int

Number of substitutions for the eigenvariable of the universally quantified variable (m)

Number of substitutions for the eigenvariable of the universally quantified variable (m)

Attributes

Source
introducePiCut.scala
val multiplicityOfBeta: Int

Number of substitutions for the eigenvariables of the existentially quantified variable independent from the substitution of the universal eigenvariable (p)

Number of substitutions for the eigenvariables of the existentially quantified variable independent from the substitution of the universal eigenvariable (p)

Attributes

Source
introducePiCut.scala
val productionRulesXS: List[(Expr, Expr)]

List of all substitution pairs (alpha,r_i) and (r_i,alpha)

List of all substitution pairs (alpha,r_i) and (r_i,alpha)

Attributes

Source
introducePiCut.scala
val productionRulesYS: List[(Expr, Expr)]

List of all substitution pairs (beta_j,t_i(alpha)) and (t_i(alpha),beta_j)

List of all substitution pairs (beta_j,t_i(alpha)) and (t_i(alpha),beta_j)

Attributes

Source
introducePiCut.scala
val reducedRepresentationToFormula: Formula

Transforms the reduced representation from a sequent to a formula

Transforms the reduced representation from a sequent to a formula

Attributes

Source
introducePiCut.scala
val substitutionPairsAlpha: List[(Expr, Expr)]

Pairs of the universal eigenvariable with the substitutions for the universal eigenvariable ((alpha,r_1),...,(alpha,r_m))

Pairs of the universal eigenvariable with the substitutions for the universal eigenvariable ((alpha,r_1),...,(alpha,r_m))

Attributes

Source
introducePiCut.scala
val substitutionPairsBeta: List[(Expr, Expr)]

Pairs of the existential eigenvariables with the substitutions for the existential eigenvariables ((beta_1,t_1(alpha)),...,(beta_1,t_p(alpha)),...,(beta_m,t_1(alpha)),...,(beta_m,t_p(alpha)))

Pairs of the existential eigenvariables with the substitutions for the existential eigenvariables ((beta_1,t_1(alpha)),...,(beta_1,t_p(alpha)),...,(beta_m,t_1(alpha)),...,(beta_m,t_p(alpha)))

Attributes

Source
introducePiCut.scala
val substitutionsAlpha: List[Substitution]

List of substitutions ((alpha->r_1),...,(alpha->r_m))

List of substitutions ((alpha->r_1),...,(alpha->r_m))

Attributes

Source
introducePiCut.scala
Generated with