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
- 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))
- Source
- introducePiCut.scala
- Alphabetic
- By Inheritance
- Pi2SeHs
- Serializable
- Product
- Equals
- AnyRef
- Any
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new Pi2SeHs(reducedRepresentation: Sequent[Formula], universalEigenvariable: Var, existentialEigenvariables: List[Var], substitutionsForAlpha: List[Expr], substitutionsForBetaWithAlpha: List[Expr])
- 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))
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- def +(other: String): String
- def ->[B](y: B): (Pi2SeHs, B)
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @native() @IntrinsicCandidate()
- val dualNonTautologicalAxioms: List[Sequent[Formula]]
The set of all relevant normalized (everything is shifted to the left side) leaves
- def ensuring(cond: (Pi2SeHs) => Boolean, msg: => Any): Pi2SeHs
- def ensuring(cond: (Pi2SeHs) => Boolean): Pi2SeHs
- def ensuring(cond: Boolean, msg: => Any): Pi2SeHs
- def ensuring(cond: Boolean): Pi2SeHs
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- val existentialEigenvariables: List[Var]
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @IntrinsicCandidate()
- def herbrandSequent(): Sequent[Formula]
Computes the Herbrand sequent that corresponds to the schematic Pi-2 grammar (F[x\T_1] |- G[y\T_2])
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- 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
- 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
- val multiplicityOfAlpha: Int
Number of substitutions for the eigenvariable of the universally quantified variable (m)
- val multiplicityOfBeta: Int
Number of substitutions for the eigenvariables of the existentially quantified variable independent from the substitution of the universal eigenvariable (p)
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @IntrinsicCandidate()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @IntrinsicCandidate()
- def productElementNames: Iterator[String]
- Definition Classes
- Product
- val productionRulesXS: List[(Expr, Expr)]
List of all substitution pairs (alpha,r_i) and (r_i,alpha)
- val productionRulesYS: List[(Expr, Expr)]
List of all substitution pairs (beta_j,t_i(alpha)) and (t_i(alpha),beta_j)
- val reducedRepresentation: Sequent[Formula]
- val reducedRepresentationToFormula: Formula
Transforms the reduced representation from a sequent to a formula
- 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
- val substitutionPairsAlpha: List[(Expr, Expr)]
Pairs of the universal eigenvariable with the substitutions for the universal eigenvariable ((alpha,r_1),...,(alpha,r_m))
- 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)))
- 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)
- index
Indicates the considered existential eigenvariable (1 <= index <= m)
- val substitutionsAlpha: List[Substitution]
List of substitutions ((alpha->r_1),...,(alpha->r_m))
- 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)
- index
Indicates the considered existential eigenvariable (1 <= index <= m)
- val substitutionsForAlpha: List[Expr]
- val substitutionsForBetaWithAlpha: List[Expr]
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- 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)
- unifiedLiterals
A set of formulas (unified literals) that define the reduced signature/language
- val universalEigenvariable: Var
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
- def formatted(fmtstr: String): String
- Implicit
- This member is added by an implicit conversion from Pi2SeHs toStringFormat[Pi2SeHs] performed by method StringFormat in scala.Predef.
- Definition Classes
- StringFormat
- Annotations
- @deprecated @inline()
- Deprecated
(Since version 2.12.16) Use
formatString.format(value)instead ofvalue.formatted(formatString), or use thef""string interpolator. In Java 15 and later,formattedresolves to the new method in String which has reversed parameters.
- def →[B](y: B): (Pi2SeHs, B)
- Implicit
- This member is added by an implicit conversion from Pi2SeHs toArrowAssoc[Pi2SeHs] performed by method ArrowAssoc in scala.Predef.
- Definition Classes
- ArrowAssoc
- Annotations
- @deprecated
- Deprecated
(Since version 2.13.0) Use
->instead. If you still wish to display it as one character, consider using a font with programming ligatures such as Fira Code.
This is the API documentation for GAPT.
The main package is gapt.