abstract class BinaryCertificate extends Certificate
Abstract superclass of certificates with two children
- Alphabetic
- By Inheritance
- BinaryCertificate
- Certificate
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new BinaryCertificate(leftChild: Certificate, rightChild: Certificate, order: TermOrder)
Abstract Value Members
- abstract val localAssumedFormulas: Set[CertFormula]
- Definition Classes
- Certificate
- abstract val localProvidedFormulas: Seq[Set[CertFormula]]
Formulae that are introduced into the antecedent by this rule application (one set for each subproof).
Formulae that are introduced into the antecedent by this rule application (one set for each subproof). This will implicitly simplify formulae (all simplifications that are built into the datastructures are carried out).
- Definition Classes
- Certificate
- abstract def update(newSubCerts: Seq[Certificate]): Certificate
- Definition Classes
- Certificate
Concrete Value Members
- def apply(i: Int): Certificate
- Definition Classes
- BinaryCertificate → Certificate
- lazy val assumedFormulas: Set[CertFormula]
Formulae that the proof assumes to be present on this branch (i.e., premisses of rules applied in the proof).
Formulae that the proof assumes to be present on this branch (i.e., premisses of rules applied in the proof). We assume that all formulae live in the antecedent.
- Definition Classes
- Certificate
- val closingConstraint: Conjunction
The constraint resulting from this proof
The constraint resulting from this proof
- Definition Classes
- BinaryCertificate → Certificate
- lazy val constants: Set[ConstantTerm]
Set of constants occurring in this certificate.
Set of constants occurring in this certificate. By default this will contain the set of all constants in sub-certificates, as well as constants in assumed formulas.
- Definition Classes
- Certificate
- lazy val inferenceCount: Int
- Definition Classes
- Certificate
- def iterator: Iterator[Certificate]
- Definition Classes
- BinaryCertificate → Certificate
- val leftChild: Certificate
- def length: Int
- Definition Classes
- BinaryCertificate → Certificate
- val localBoundConstants: Set[ConstantTerm]
Constants bound by the root operator of the certificate.
Constants bound by the root operator of the certificate.
- Definition Classes
- Certificate
- val order: TermOrder
- Definition Classes
- BinaryCertificate → Certificate
- val rightChild: Certificate
- def size: Int
- Definition Classes
- Certificate
- def subCertificates: IndexedSeq[Certificate]
- Definition Classes
- Certificate
- lazy val theoryAxioms: Set[CertFormula]
- Definition Classes
- Certificate