final case class Polarity(inSuc: Boolean) extends AnyVal with Product with Serializable
Polarity of a formula.
There are two polarities, positive/in-succedent and negative/in-antecedent. Polarities serve multiple purposes:
- They distinguish strong and weak quantifiers. A universal (∀) quantifier in positive/in-succedent polarity is strong (requires an eigenvariable/Skolem inference), and is weak in negative/in-antecedent polarity (can be instantiated with any term).
- They guide the construction of expansion trees and their deep formulas. A merge in positive polarity has a disjunction as deep formula, in negative polarity it has a conjunction.
- They specify the side/cedent of a sequent.
Our convention is based on proofs in LK:
- formulas in the succedent are positive
- formulas in the antecedent are negative
This is used consistently, except for a major exception: in resolution proofs, the polarity is reversed. A formula in the antecedent of a clause in a resolution proof has the negative/in-antecedent polarity (as it is in the antecedent of a sequent). However upon conversion to LK/ET, the polarity switches to positive/in-succedent polarity.
- Source
- Polarity.scala
- Alphabetic
- By Inheritance
- Polarity
- Serializable
- Product
- Equals
- AnyVal
- Any
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
- Public
- Protected
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- Any
- final def ##: Int
- Definition Classes
- Any
- def +(other: String): String
- def ->[B](y: B): (Polarity, B)
- final def ==(arg0: Any): Boolean
- Definition Classes
- Any
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def ensuring(cond: (Polarity) => Boolean, msg: => Any): Polarity
- def ensuring(cond: (Polarity) => Boolean): Polarity
- def ensuring(cond: Boolean, msg: => Any): Polarity
- def ensuring(cond: Boolean): Polarity
- def getClass(): Class[_ <: AnyVal]
- Definition Classes
- AnyVal → Any
- def inAnt: Boolean
- val inSuc: Boolean
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def negative: Boolean
- def positive: Boolean
- def productElementNames: Iterator[String]
- Definition Classes
- Product
- def toString(): String
- Definition Classes
- Polarity → Any
- def unary_!: Polarity
Deprecated Value Members
- def formatted(fmtstr: String): String
- Implicit
- This member is added by an implicit conversion from Polarity toStringFormat[Polarity] 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): (Polarity, B)
- Implicit
- This member is added by an implicit conversion from Polarity toArrowAssoc[Polarity] 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.