Type Members

1.  case class Ant(k: Int) extends SequentIndex with Product with Serializable
2.  trait Checkable[-T] extends AnyRef
3.  type Clause[+A] = Sequent[A]
4.  trait ContextRule[Formula, This <: SequentProof[Formula, This]] extends SequentProof[Formula, This]
5.  class ContextSection extends AnyRef
6.  trait DagProof[Proof <: DagProof[Proof]] extends Product

   DAG-like proof.

   DAG-like proof.

   Proofs are recursive structures that are represented as case classes. Equality is standard case class equality (but implemented in such a way that it is efficient on DAGs).

   Proof

   The type of proof, e.g. gapt.proofs.lk.LKProof.

7.  type FOLClause = Sequent[FOLAtom]
8.  type FOLSequent = Sequent[FOLFormula]
9.  type HOLClause = Sequent[Atom]
10.  type HOLSequent = Sequent[Formula]
11.  sealed trait IndexOrFormula extends AnyRef
12.  type Label = String
13.  type LabelledFormula = (Label, Formula)
14.  type LabelledSequent = Sequent[LabelledFormula]
15.  case class NDSequent[+A](assumptions: Seq[A], conclusion: A) extends Product with Serializable

    Sequents for natural deduction.

    Sequents for natural deduction.

    They have the form A₁,...,A_m :- B (there is always exactly one element in the succedent).

    A

    The type of elements in the sequent.

    assumptions

    The elements A₁,...,A_m.

    conclusion

    The element B.

16.  class ProofBuilder[+Proof] extends AnyRef

    Class for convenient construction of proofs.

    Class for convenient construction of proofs. Allows you to write proofs post-order style (à la Bussproofs). Example:

    (ProofBuilder
    c LogicalAxiom(A)
    c LogicalAxiom(B)
    u (WeakeningLeftRule(_, C))
    b (AndRightRule(_,_, And(A, B))
    qed)
    

    The constructor is private, so the only way to instantiate this class is by using the ProofBuilder object. This means that the stack will always be empty in the beginning.

17.  implicit final class RichClause[+A] extends AnyVal
18.  implicit final class RichFOLSequent extends AnyVal
19.  implicit final class RichFormulaSequent extends AnyVal
20.  implicit final class SeqWrapper[+A] extends AnyVal
21.  case class Sequent[+A](antecedent: Vector[A], succedent: Vector[A]) extends Product with Serializable

    A sequent is a pair of sequences of elements of type A, typically written as a₁,…,a_m :- b₁,…,b_n.

    A sequent is a pair of sequences of elements of type A, typically written as a₁,…,a_m :- b₁,…,b_n.

    A

    The type of the elements of the sequent.

    antecedent

    The first list.

    succedent

    The second list.

22.  case class SequentConnector(lowerSizes: (Int, Int), upperSizes: (Int, Int), parentsSequent: Sequent[Seq[SequentIndex]]) extends Product with Serializable

    This class models the connection of formula occurrences between two sequents in a proof.

    This class models the connection of formula occurrences between two sequents in a proof.

    The most basic use case is that of connecting the conclusion of an LK inference with one of the premises. This is the origin of the names "lowerSizes" and "upperSizes".

    lowerSizes

    The dimensions of the first ("lower") of the two connected sequents.

    upperSizes

    The dimensions of the second ("upper") of the two connected sequents.

    parentsSequent

    A sequent of lists of indices such that for each index i of lowerSequent, parentsSequent(i) is the list of indices of the parents of i in upperSequent.

23.  implicit final class SequentFlatMapOp[A] extends AnyVal
24.  implicit final class SequentFlattenOp[A] extends AnyVal
25.  sealed abstract class SequentIndex extends Ordered[SequentIndex]

    Represents an index of an element in a sequent.

    Represents an index of an element in a sequent.

    In a sequent, the elements have the following indices: Ant(0), Ant(1), ..., Ant(m) :- Suc(0), Suc(1), ..., Suc(n)

26.  trait SequentProof[+Formula, This <: SequentProof[Formula, This]] extends DagProof[This]
27.  case class SetSequent[+A](sequent: Sequent[A]) extends Product with Serializable

    Used for clause set extraction

    Used for clause set extraction

    sequent

    A sequent.

28.  case class Suc(k: Int) extends SequentIndex with Product with Serializable