nd

package nd

Source: package.scala

Linear Supertypes

AnyRef, Any

Content Hierarchy

Ordering

Alphabetic
By Inheritance

Inherited

nd
AnyRef
Any

Hide All
Show All

Visibility

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 π₁.
rightSubProof
The proof π₂.
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 B
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 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 π₁.
rightSubProof
The proof π₂.
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 x_i and y_i are eigenvariables; x_i are the eigenvariables of the same type as the inductive data type, y_i 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(x₁), ..., F(x_n)
eigenVars
The eigenvariables of this case: x₁, ..., x_n, y₁, ..., y_n (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 π₁.
rightSubProof
The proof π₂.
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 π₁.
middleSubProof
The proof π₂.
aux1
The index of A.
rightSubProof
The proof π₃.
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]

Packages

nd

package nd

Type Members

Value Members

Inherited from AnyRef

Inherited from Any

Ungrouped

Packages

nd

package nd

Type Members

Value Members

Inherited from AnyRef

Inherited from Any

Ungrouped

nd