package logic
- Source
- package.scala
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- logic
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- Protected
Type Members
- final case class Polarity(inSuc: Boolean) extends AnyVal with Product with Serializable
Polarity of a formula.
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.
Value Members
- def argumentVariablesWithPatternFor(pattern: (Int) => String)(constant: Const): Seq[Var]
- def disjointnessAxiom(constructor1: Const, constructor2: Const): Formula
- def disjointnessAxioms(inductiveType: InductiveType): Iterable[Formula]
- def injectivityAxiom(constructor: Const): Formula
- def injectivityAxioms(inductiveType: InductiveType): Iterable[Formula]
- def isPolyadic(constant: Const): Boolean
- def projectorDefinitionRules(it: InductiveType): Iterable[ReductionRule]
- def projectorDefinitions(it: InductiveType): Iterable[Formula]
- object AllDistinct
- object EqualityReflexivity
- object EqualityTransitivity
- object FunctionCongruence
- object Polarity extends Serializable
- object PredicateCongruence
- object clauseSubsumption
- object toImplications
This is the API documentation for GAPT.
The main package is gapt.