Class/Object

ap.proof.certificates

Certificate

Related Docs: object Certificate | package certificates

Permalink

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, OmegaCertificate, ReferenceCertificate, 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. All

Instance Constructors

  1. new Certificate()

    Permalink

Abstract Value Members

  1. abstract def apply(i: Int): Certificate

    Permalink

  2. abstract val closingConstraint: Conjunction

    Permalink

    The constraint resulting from this proof

  3. abstract def iterator: Iterator[Certificate]

    Permalink

  4. abstract def length: Int

    Permalink

  5. abstract val localAssumedFormulas: Set[CertFormula]

    Permalink

  6. abstract val localProvidedFormulas: Seq[Set[CertFormula]]

    Permalink

    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

    Permalink

  8. abstract def update(newSubCerts: Seq[Certificate]): Certificate

    Permalink

Concrete Value Members

  1. final def !=(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any

  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any

  3. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any

  4. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any

  5. lazy val assumedFormulas: Set[CertFormula]

    Permalink

    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

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @throws( ... )

  7. lazy val constants: Set[ConstantTerm]

    Permalink

    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

    Permalink
    Definition Classes
    AnyRef

  9. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any

  10. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  11. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  12. lazy val inferenceCount: Int

    Permalink

  13. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any

  14. val localBoundConstants: Set[ConstantTerm]

    Permalink

    Constants bound by the root operator of the certificate.

  15. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef

  16. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  17. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  18. def size: Int

    Permalink

  19. def subCertificates: IndexedSeq[Certificate]

    Permalink

  20. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef

  21. lazy val theoryAxioms: Set[CertFormula]

    Permalink

  22. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any

  23. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

  24. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

  25. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Deprecated Value Members

  1. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
    Deprecated

    (Since version ) see corresponding Javadoc for more information.

Inherited from AnyRef

Inherited from Any

Ungrouped