class PartialInferenceCertificate extends PartialCertificate
Partial certificate prepending given inferences to some certificate.
- Alphabetic
- By Inheritance
- PartialInferenceCertificate
- PartialCertificate
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new PartialInferenceCertificate(inferences: BranchInferenceCollection, order: TermOrder)
- Attributes
- protected[certificates]
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- def after(those: Seq[PartialCertificate]): PartialCertificate
- Definition Classes
- PartialCertificate
- def andThen(inferences: BranchInferenceCollection, order: TermOrder): PartialCertificate
- Definition Classes
- PartialCertificate
- def apply(subCerts: Seq[Certificate]): Certificate
- Definition Classes
- PartialInferenceCertificate → PartialCertificate
- val arity: Int
- Definition Classes
- PartialInferenceCertificate → PartialCertificate
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def bindFirst(cert: Certificate): Either[PartialCertificate, Certificate]
Bind the first argument of the partial certificate, resulting in a partial certificate with one fewer free arguments, or (in case proof pruning can be performed) a complete certificate
Bind the first argument of the partial certificate, resulting in a partial certificate with one fewer free arguments, or (in case proof pruning can be performed) a complete certificate
- Definition Classes
- PartialInferenceCertificate → PartialCertificate
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- def dfExplore(certBuilder: CertBuilder, lemmaBase: LemmaBase, lemmaBaseAssumedInferences: Int): Certificate
Construct a full certificate, by creating the required child certificates on demand.
Construct a full certificate, by creating the required child certificates on demand. The given functions are supposed to produce either a certificate for a certain subtree, or
nullin case no certificate exists. The method as a whole will also returnnullif no complete certificate could be constructed.- Definition Classes
- PartialInferenceCertificate → PartialCertificate
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- val inferences: BranchInferenceCollection
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def shuffle(implicit randomDataSource: RandomDataSource): (PartialInferenceCertificate, List[Int])
Shuffle the certificates expected by this partial certificate, and return the new order of arguments relatively to the old order.
Shuffle the certificates expected by this partial certificate, and return the new order of arguments relatively to the old order.
- Definition Classes
- PartialInferenceCertificate → PartialCertificate
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- AnyRef → Any
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)