abstract class Certificate extends AnyRef

Datastructures used to express and extract whole, detailed proofs, which can independently be checked and be used for further processing (e.g., to compute interpolants). Certificates are trees/proof terms, with the following class as the abstract superclass of all tree nodes. Proofs are more or less tableau proofs, with rule applications assuming certain formulae on a branch and producing new formulae.

Linear Supertypes
AnyRef, Any
Known Subclasses
BetaCertificate, BinaryCertificate, BranchInferenceCertificate, CertificateOneChild, CloseCertificate, CutCertificate, ReferenceCertificate, OmegaCertificate, SplitEqCertificate, StrengthenCertificate
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Certificate
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Instance Constructors

  1. new Certificate()

Abstract Value Members

  1. abstract def apply(i: Int): Certificate
  2. abstract val closingConstraint: Conjunction

    The constraint resulting from this proof

  3. abstract def iterator: Iterator[Certificate]
  4. abstract def length: Int
  5. abstract val localAssumedFormulas: Set[CertFormula]
  6. 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).

  7. abstract val order: TermOrder
  8. abstract def update(newSubCerts: Seq[Certificate]): Certificate

Concrete Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. 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.

  6. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  7. 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.

  8. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  9. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  10. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  11. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  12. lazy val inferenceCount: Int
  13. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  14. val localBoundConstants: Set[ConstantTerm]

    Constants bound by the root operator of the certificate.

  15. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  16. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  17. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  18. def size: Int
  19. def subCertificates: IndexedSeq[Certificate]
  20. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  21. lazy val theoryAxioms: Set[CertFormula]
  22. def toString(): String
    Definition Classes
    AnyRef → Any
  23. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  24. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  25. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

    (Since version 9)

Inherited from AnyRef

Inherited from Any

Ungrouped