package nd
- Alphabetic
- By Inheritance
- nd
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Type Members
- case class AndElim1Rule(subProof: NDProof) extends UnaryNDProof with CommonRule with Product with Serializable
An NDProof ending with elimination of the right conjunct:
(π) Γ :- A ∧ B --------------∧:e1 Γ :- A
An NDProof ending with elimination of the right conjunct:
(π) Γ :- A ∧ B --------------∧:e1 Γ :- A
- subProof
The subproof π.
- case class AndElim2Rule(subProof: NDProof) extends UnaryNDProof with CommonRule with Product with Serializable
An NDProof ending with elimination of the left conjunct:
(π) Γ :- A ∧ B --------------∧:e2 Γ :- B
An NDProof ending with elimination of the left conjunct:
(π) Γ :- A ∧ B --------------∧:e2 Γ :- B
- subProof
The subproof π.
- case class AndIntroRule(leftSubProof: NDProof, rightSubProof: NDProof) extends BinaryNDProof with CommonRule with Product with Serializable
An NDProof ending with a conjunction on the right:
(π1) (π2) Γ :- A Π :- B --------------------∧:i Γ, Π :- A∧B
An NDProof ending with a conjunction on the right:
(π1) (π2) Γ :- A Π :- B --------------------∧:i Γ, Π :- A∧B
- leftSubProof
The proof π1.
- rightSubProof
The proof π2.
- abstract class BinaryNDProof extends NDProof
An NDProof deriving a sequent from two other sequents:
(π1) (π2) Γ :- A Γ' :- A' ------------------ Π :- B
- case class BottomElimRule(subProof: NDProof, mainFormula: Formula) extends UnaryNDProof with CommonRule with Product with Serializable
An NDProof eliminating ⊥:
(π) Γ :- ⊥ --------⊥:e Γ :- A
An NDProof eliminating ⊥:
(π) Γ :- ⊥ --------⊥:e Γ :- A
- subProof
The subproof π.
- mainFormula
The formula A.
- trait CommonRule extends NDProof with ContextRule[Formula, NDProof]
- case class ContractionRule(subProof: NDProof, aux1: SequentIndex, aux2: SequentIndex) extends UnaryNDProof with CommonRule with Product with Serializable
An NDProof ending with a contraction:
(π) A, A, Γ :- B --------------ctr A, Γ :- B
An NDProof ending with a contraction:
(π) A, A, Γ :- B --------------ctr A, Γ :- B
- subProof
The subproof π.
- aux1
The index of one occurrence of A.
- aux2
The index of the other occurrence of A.
- class ConvenienceConstructor extends AnyRef
Class for reducing boilerplate code in ND companion objects.
- case class DefinitionRule(subProof: NDProof, mainFormula: Formula) extends UnaryNDProof with CommonRule with Product with Serializable
An NDProof ending with a definition
An NDProof ending with a definition
(π) Γ :- A[φ] -----------d Γ :- A[c]
- subProof
The proof π.
- mainFormula
The formula A[c].
- trait Eigenvariable extends AnyRef
Use this trait for rules that use eigenvariables.
- case class EqualityElimRule(leftSubProof: NDProof, rightSubProof: NDProof, formulaA: Formula, variablex: Var) extends BinaryNDProof with CommonRule with Product with Serializable
An NDProof ending with elimination of equality:
(π1) (π2) Γ :- s = t Π :- A[x\s] ------------------------------eq:e Γ,Π :- A[x\t]
An NDProof ending with elimination of equality:
(π1) (π2) Γ :- s = t Π :- A[x\s] ------------------------------eq:e Γ,Π :- A[x\t]
- leftSubProof
The subproof π1.
- rightSubProof
The subproof π2.
- formulaA
The formula A.
- variablex
The variable x.
- case class EqualityIntroRule(t: Expr) extends InitialSequent with Product with Serializable
An NDProof that consist of the introduction of an equality.
An NDProof that consist of the introduction of an equality.
----------eq:i :- t = t
- t
The term t.
- case class ExcludedMiddleRule(leftSubProof: NDProof, aux1: SequentIndex, rightSubProof: NDProof, aux2: SequentIndex) extends BinaryNDProof with CommonRule with Product with Serializable
An NDProof ending with excluded middle:
(π1) (π2) Γ, A :- B Π, ¬A :- B -------------------------EM Γ, Π :- B
An NDProof ending with excluded middle:
(π1) (π2) Γ, A :- B Π, ¬A :- B -------------------------EM Γ, Π :- B
- leftSubProof
The proof π1.
- aux1
The index of A.
- rightSubProof
The proof π2.
- aux2
The index of ¬A.
- case class ExistsElimRule(leftSubProof: NDProof, rightSubProof: NDProof, aux: SequentIndex, eigenVariable: Var) extends BinaryNDProof with CommonRule with Eigenvariable with Product with Serializable
An NDProof ending with an existential quantifier elimination:
(π1) (π2) Γ :- ∃x.A Π, A[x\α] :- B ----------------------------∃:e Γ, Π :- B
This rule is only applicable if the eigenvariable condition is satisfied: α must not occur freely in Π, and BAn NDProof ending with an existential quantifier elimination:
(π1) (π2) Γ :- ∃x.A Π, A[x\α] :- B ----------------------------∃:e Γ, Π :- B
This rule is only applicable if the eigenvariable condition is satisfied: α must not occur freely in Π, and B- leftSubProof
The proof π1.
- rightSubProof
The proof π2.
- aux
The index of A[x\α].
- eigenVariable
The variable α.
- case class ExistsIntroRule(subProof: NDProof, A: Formula, term: Expr, v: Var) extends UnaryNDProof with CommonRule with Product with Serializable
An NDProof ending with an existential quantifier introduction:
(π) Γ :- A[x\t] ------------∃:i Γ :- ∃x.A
An NDProof ending with an existential quantifier introduction:
(π) Γ :- A[x\t] ------------∃:i Γ :- ∃x.A
- subProof
The proof π.
- A
The formula A.
- term
The term t.
- v
The variable x.
- case class ForallElimRule(subProof: NDProof, term: Expr) extends UnaryNDProof with CommonRule with Product with Serializable
An NDProof ending with a universal quantifier elimination:
(π) Γ :- ∀x.A -------------∀:e Γ :- A[x\t]
An NDProof ending with a universal quantifier elimination:
(π) Γ :- ∀x.A -------------∀:e Γ :- A[x\t]
- subProof
The proof π.
- term
The term t.
- case class ForallIntroRule(subProof: NDProof, eigenVariable: Var, quantifiedVariable: Var) extends UnaryNDProof with CommonRule with Eigenvariable with Product with Serializable
An NDProof ending with a universal quantifier introduction:
(π) Γ :- A[x\α] -------------∀:i Γ :- ∀x.A
This rule is only applicable if the eigenvariable condition is satisfied: α must not occur freely in Γ.An NDProof ending with a universal quantifier introduction:
(π) Γ :- A[x\α] -------------∀:i Γ :- ∀x.A
This rule is only applicable if the eigenvariable condition is satisfied: α must not occur freely in Γ.- subProof
The proof π.
- eigenVariable
The variable α.
- quantifiedVariable
The variable x.
- case class ImpElimRule(leftSubProof: NDProof, rightSubProof: NDProof) extends BinaryNDProof with CommonRule with Product with Serializable
An NDProof ending with elimination of an implication:
(π1) (π2) Γ :- A→B Π :- A --------------------→:e Γ, Π :- B
An NDProof ending with elimination of an implication:
(π1) (π2) Γ :- A→B Π :- A --------------------→:e Γ, Π :- B
- leftSubProof
The proof π1.
- rightSubProof
The proof π2.
- case class ImpIntroRule(subProof: NDProof, aux: SequentIndex) extends UnaryNDProof with CommonRule with Product with Serializable
An NDProof ending with introduction of an implication:
(π) A, Γ :- B ------------→:i Γ :- A → B
An NDProof ending with introduction of an implication:
(π) A, Γ :- B ------------→:i Γ :- A → B
- subProof
The subproof π.
- aux
The index of A.
- case class InductionCase(proof: NDProof, constructor: Const, hypotheses: List[SequentIndex], eigenVars: List[Var]) extends Product with Serializable
Proof that a given data type constructor c preserves a formula F:
Proof that a given data type constructor c preserves a formula F:
(π) F(x,,1,,), F(x,,2,,), ..., F(x,,n,,), Γ :- F(c(x,,1,,,...,x,,n,,,y,,1,,,...,y,,n,,))
The variables xi and yi are eigenvariables; xi are the eigenvariables of the same type as the inductive data type, yi are the other arguments of the constructor c. They can come in any order in the constructor.
- proof
The NDProof ending in the sequent of this case.
- constructor
The constructor c of the inductive data type that we're considering.
- hypotheses
Indices of F(x1), ..., F(xn)
- eigenVars
The eigenvariables of this case: x1, ..., xn, y1, ..., yn (these need to correspond to the order in c)
- case class InductionRule(cases: Seq[InductionCase], formula: Abs, term: Expr) extends NDProof with CommonRule with Product with Serializable
An NDProof ending with an induction rule:
(π,,1,,) (π,,2,,) (π,,n,,) case 1 case 2 ... case n -------------------------------------(ind) Γ :- F(t: indTy)
An NDProof ending with an induction rule:
(π,,1,,) (π,,2,,) (π,,n,,) case 1 case 2 ... case n -------------------------------------(ind) Γ :- F(t: indTy)
This induction rule can handle inductive data types. The cases are proofs that the various type constructors preserve the formula we want to prove. They are provided via the InductionCase class.
- cases
A sequence of proofs showing that each type constructor preserves the validity of the main formula.
- formula
The formula we want to prove via induction.
- abstract class InitialSequent extends NDProof
An NDProof consisting of a single sequent:
--------ax Γ :- A
- case class LogicalAxiom(A: Formula) extends InitialSequent with Product with Serializable
An NDProof consisting of a logical axiom:
--------ax A :- A
An NDProof consisting of a logical axiom:
--------ax A :- A
- A
The formula A.
- abstract class NDProof extends SequentProof[Formula, NDProof]
- class NDRuleCreationException extends Exception
- case class NegElimRule(leftSubProof: NDProof, rightSubProof: NDProof) extends BinaryNDProof with CommonRule with Product with Serializable
An NDProof ending with elimination of a negation:
(π1) (π2) Γ :- ¬A Π :- A -------------------¬:e Γ, Π :- ⊥
An NDProof ending with elimination of a negation:
(π1) (π2) Γ :- ¬A Π :- A -------------------¬:e Γ, Π :- ⊥
- leftSubProof
The proof π1.
- rightSubProof
The proof π2.
- case class NegIntroRule(subProof: NDProof, aux: SequentIndex) extends UnaryNDProof with CommonRule with Product with Serializable
An NDProof ending with introduction of a negation:
(π) A, Γ :- ⊥ -----------¬:i Γ :- ¬A
An NDProof ending with introduction of a negation:
(π) A, Γ :- ⊥ -----------¬:i Γ :- ¬A
- subProof
The subproof π.
- aux
The index of A.
- case class OrElimRule(leftSubProof: NDProof, middleSubProof: NDProof, aux1: SequentIndex, rightSubProof: NDProof, aux2: SequentIndex) extends TernaryNDProof with CommonRule with Product with Serializable
An NDProof ending with elimination of a disjunction:
(π1) (π2) (π3) Γ :- A∨B Π, A :- C Δ, B :- C ------------------------------------∨:e Γ, Π, Δ :- C
An NDProof ending with elimination of a disjunction:
(π1) (π2) (π3) Γ :- A∨B Π, A :- C Δ, B :- C ------------------------------------∨:e Γ, Π, Δ :- C
- leftSubProof
The proof π1.
- middleSubProof
The proof π2.
- aux1
The index of A.
- rightSubProof
The proof π3.
- aux2
The index of B.
- case class OrIntro1Rule(subProof: NDProof, rightDisjunct: Formula) extends UnaryNDProof with CommonRule with Product with Serializable
An NDProof ending with introduction of a disjunction, with a new formula as the right disjunct:
(π) Γ :- A ------------∨:i1 Γ :- A ∨ B
An NDProof ending with introduction of a disjunction, with a new formula as the right disjunct:
(π) Γ :- A ------------∨:i1 Γ :- A ∨ B
- subProof
The subproof π.
- rightDisjunct
The formula B.
- case class OrIntro2Rule(subProof: NDProof, leftDisjunct: Formula) extends UnaryNDProof with CommonRule with Product with Serializable
An NDProof ending with introduction of a disjunction, with a new formula as the left disjunct:
(π) Γ :- A ------------∨:i2 Γ :- B ∨ A
An NDProof ending with introduction of a disjunction, with a new formula as the left disjunct:
(π) Γ :- A ------------∨:i2 Γ :- B ∨ A
- subProof
The subproof π.
- leftDisjunct
The formula B.
- abstract class TernaryNDProof extends NDProof
An NDProof deriving a sequent from three other sequents:
(π1) (π2) (π3) Γ1 :- A1 Γ2 :- A2 Γ3 :- A3 -------------------------------- Π :- B
- case class TheoryAxiom(mainFormula: Formula) extends InitialSequent with Product with Serializable
An NDProof consisting of an axiom from a theory:
--------th :- A
An NDProof consisting of an axiom from a theory:
--------th :- A
- mainFormula
The axiom A.
- abstract class UnaryNDProof extends NDProof
An NDProof deriving a sequent from another sequent:
(π) Γ :- A ---------- Γ' :- A'
- case class WeakeningRule(subProof: NDProof, formula: Formula) extends UnaryNDProof with CommonRule with Product with Serializable
An NDProof ending with weakening:
(π) Γ :- B ---------wkn A, Γ :- B
An NDProof ending with weakening:
(π) Γ :- B ---------wkn A, Γ :- B
- subProof
The subproof π.
- formula
The formula A.
Value Members
- implicit val ndSubstitutable: ClosedUnderSub[NDProof]
- object BinaryNDProof
- object ContractionRule extends ConvenienceConstructor with Serializable
- object EqualityElimRule extends ConvenienceConstructor with Serializable
- object ExistsElimRule extends ConvenienceConstructor with Serializable
- object ExistsIntroRule extends ConvenienceConstructor with Serializable
- object ForallElimBlock
- object ForallIntroRule extends ConvenienceConstructor with Serializable
- object ImpIntroRule extends ConvenienceConstructor with Serializable
- object InitialSequent
- object LogicalAxiom extends ConvenienceConstructor with Serializable
- object MRealizability
- object NegIntroRule extends ConvenienceConstructor with Serializable
- object OrElimRule extends ConvenienceConstructor with Serializable
- object TernaryNDProof
- case object TopIntroRule extends InitialSequent with Product with Serializable
An NDProof that is the introduction of ⊤:
------⊤:i :- ⊤
- object UnaryNDProof
- object WeakeningRule extends ConvenienceConstructor with Serializable
- implicit object casesReplaceable extends ClosedUnderReplacement[InductionCase]
- object freeVariablesND
- object friedman
- object kolmogorov
- implicit object replaceable extends ClosedUnderReplacement[NDProof]
This is the API documentation for GAPT.
The main package is gapt.